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

Simple item page
dc.contributor.advisorGeldenhuys, Jaco
dc.contributor.authorSeotsanyana, Motlatsien_ZA
dc.contributor.otherUniversity of Stellenbosch. Faculty of Science. Dept. of Mathematical Sciences.
dc.date.accessioned2008-04-10T10:17:25Zen_ZA
dc.date.accessioned2010-06-01T08:41:53Z
dc.date.available2008-04-10T10:17:25Zen_ZA
dc.date.available2010-06-01T08:41:53Z
dc.date.issued2007-12
dc.descriptionThesis (MSc (Mathematical Sciences))--University of Stellenbosch, 2007.
dc.description.abstractThe 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.en_ZA
dc.format.extent625571 bytesen_ZA
dc.format.mimetypeapplication/pdfen_ZA
dc.identifier.urihttp://hdl.handle.net/10019.1/2162
dc.language.isoenen_ZA
dc.publisherStellenbosch : University of Stellenbosch
dc.rights.holderUniversity of Stellenbosch
dc.subjectTheses -- Mathematicsen_ZA
dc.subjectDissertations -- Mathematicsen_ZA
dc.subjectTheses -- Computer scienceen_ZA
dc.subjectDissertations -- Computer scienceen_ZA
dc.subject.lcshSoftware protection -- Mathematical modelsen_ZA
dc.subject.lcshComputer security -- Case studies.en_ZA
dc.subject.lcshFormal methods (Computer science)en_ZA
dc.subject.otherMathematical Sciencesen_ZA
dc.subject.otherComputer Scienceen_ZA
dc.titleFormal specification and verification of safety interlock systems: A comparative case studyen_ZA
dc.typeThesisen_ZA
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
seotsanyana_formal_2007.pdf
Size:
610.91 KB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
1.72 KB
Format:
Plain Text
Description:
Download
Collections
Masters Degrees (Mathematical Sciences)