Formal specification and verification of safety interlock systems: A comparative case study

[摘要] The ever-increasing reliance of society on computer systems has led to a need for highly reliablesystems. There are a number of areas where computer systems perform critical functions andthe development of such systems requires a higher level of attention than any other type ofsystem. The appropriate approach in this situation is known as formal methods. Formalmethods refer to the use of mathematical techniques for the specification, development andverification of software and hardware systems. The two main goals of this thesis are:1. The design of mathematical models as a basis for the implementation of error-free softwarefor the safety interlock system at iThemba LABS (http://www.tlabs.ac.za/).2. The comparison of formal method techniques that addresses the lack of much-neededempirical studies in the field of formal methods.Mathematical models are developed using model checkers: Spin, Uppaal, Smv and a theoremprover Pvs. The criteria used for the selection of the tools was based on the popularity ofthe tools, support of the tools, representation of properties, representativeness of verificationtechniques, and ease of use.The procedure for comparing these methods is divided into two phases. Phase one involvesthe time logging of activities followed by a novice modeler to model check and theorem provesoftware systems. The results show that it takes more time to learn and use a theorem proverthan a model checker. Phase two involves the performance of the tools in relation to the timetaken to verify a property, memory used, number of states and transitions generated. In spiteof the differences between models, the results are in favor of Smv and this maybe attributedto the nature of the safety interlock system, as it involves a lot of hard-wired lines.

[发布机构] Stellenbosch University