Verification and Improvement of MINIX 3 Based on FeaVer
2010; East China Computer Technology Research Institute; Volume: 36; Issue: 22 Linguagem: Inglês
ISSN
1000-3428
Autores Tópico(s)Advanced Sensor and Control Systems
ResumoFeaVer is used to perform a formal verification of source codes of MINIX 3 file system,and the error codes are found.In the procedure of verification,the concept of test harness is introduced,whose characteristics are efficient and reproducible.The original model based on the verification results is modified and a new model is built.It is verified that the new model conforms to the correctness property specified.The source files of MINIX 3 are upgraded according to the new model to make the operating system more reliable.
Referência(s)