Formal specification and verification of safety interlock systems: A comparative case study
Date
2007-12
Authors
Seotsanyana, Motlatsi
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : University of Stellenbosch
Abstract
The ever-increasing reliance of society on computer systems has led to a need for highly reliable
systems. There are a number of areas where computer systems perform critical functions and
the development of such systems requires a higher level of attention than any other type of
system. The appropriate approach in this situation is known as formal methods. Formal
methods refer to the use of mathematical techniques for the specification, development and
verification 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 software
for 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-needed
empirical studies in the field of formal methods.
Mathematical models are developed using model checkers: Spin, Uppaal, Smv and a theorem
prover Pvs. The criteria used for the selection of the tools was based on the popularity of
the tools, support of the tools, representation of properties, representativeness of verification
techniques, and ease of use.
The procedure for comparing these methods is divided into two phases. Phase one involves
the time logging of activities followed by a novice modeler to model check and theorem prove
software systems. The results show that it takes more time to learn and use a theorem prover
than a model checker. Phase two involves the performance of the tools in relation to the time
taken to verify a property, memory used, number of states and transitions generated. In spite
of the differences between models, the results are in favor of Smv and this maybe attributed
to the nature of the safety interlock system, as it involves a lot of hard-wired lines.
Description
Thesis (MSc (Mathematical Sciences))--University of Stellenbosch, 2007.
Keywords
Theses -- Mathematics, Dissertations -- Mathematics, Theses -- Computer science, Dissertations -- Computer science