基于FeaVer的MINIX3验证和改进

使用FeaVer对MINIX3文件系统源代码进行形式化验证,并找到其中的错误代码。在验证的过程中引入测试用具的概念,它的特点是高效性和可复用性。在验证结果的基础上对原来的验证模型进行修改,并建立新的模型。经验证新模型符合应有的正确性属性。以新模型为依据对MINIX3的源代码进行改进,使操作系统达到一个更可靠的状态。

S3C44B0X的μC/OS-Ⅱ移植技术研究

在嵌入式系统的开发过程中由于操作系统的兼容性较差,经常会遇到基于一种CPU开发的操作系统不能在其他CPU上稳定的运行的情况,造成了重复开发的浪费。针对以上问题,对开放源码的μC/OS-Ⅱ实时操作系统在三星公司的S3C44B0X处理器上的移植技术和移植条件进行了分析与研究,实现了μC/OS-Ⅱ在S3C44B0X处理器上的移植,并对移植过程中的注意事项进行了讨论。实验证明,移植后的系统运行稳定和重新开发相比节省了大量时间,该移植方法对其他嵌入式操作系统的移植也有很好的借鉴作用。