Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Formal specification and verification of safety interlock systems: A comparative case study
Thesis (MSc (Mathematical Sciences))--University of Stellenbosch, 2007.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
Stellenbosch : University of Stellenbosch
2008
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867614086480527361 |
|---|---|
| access_status_str | Open Access |
| author | Seotsanyana, Motlatsi |
| author2 | Geldenhuys, Jaco |
| author_browse | Geldenhuys, Jaco Seotsanyana, Motlatsi |
| author_facet | Geldenhuys, Jaco Seotsanyana, Motlatsi |
| author_sort | Seotsanyana, Motlatsi |
| collection | Thesis |
| dc_rights_str_mv | University of Stellenbosch |
| description | Thesis (MSc (Mathematical Sciences))--University of Stellenbosch, 2007. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/2162 |
| institution | Stellenbosch University (South Africa) |
| language | English |
| last_indexed | 2026-06-10T12:46:25.318Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2008 |
| publishDateRange | 2008 |
| publishDateSort | 2008 |
| publisher | Stellenbosch : University of Stellenbosch |
| publisherStr | Stellenbosch : University of Stellenbosch |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/2162 Formal specification and verification of safety interlock systems: A comparative case study Seotsanyana, Motlatsi Geldenhuys, Jaco University of Stellenbosch. Faculty of Science. Dept. of Mathematical Sciences. Theses -- Mathematics Dissertations -- Mathematics Theses -- Computer science Dissertations -- Computer science Software protection -- Mathematical models Computer security -- Case studies. Formal methods (Computer science) Mathematical Sciences Computer Science Thesis (MSc (Mathematical Sciences))--University of Stellenbosch, 2007. 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. 2008-04-10T10:17:25Z 2010-06-01T08:41:53Z 2008-04-10T10:17:25Z 2010-06-01T08:41:53Z 2007-12 Thesis http://hdl.handle.net/10019.1/2162 en University of Stellenbosch 625571 bytes application/pdf application/pdf Stellenbosch : University of Stellenbosch |
| spellingShingle | Theses -- Mathematics Dissertations -- Mathematics Theses -- Computer science Dissertations -- Computer science Software protection -- Mathematical models Computer security -- Case studies. Formal methods (Computer science) Mathematical Sciences Computer Science Seotsanyana, Motlatsi Formal specification and verification of safety interlock systems: A comparative case study |
| title | Formal specification and verification of safety interlock systems: A comparative case study |
| title_full | Formal specification and verification of safety interlock systems: A comparative case study |
| title_fullStr | Formal specification and verification of safety interlock systems: A comparative case study |
| title_full_unstemmed | Formal specification and verification of safety interlock systems: A comparative case study |
| title_short | Formal specification and verification of safety interlock systems: A comparative case study |
| title_sort | formal specification and verification of safety interlock systems a comparative case study |
| topic | Theses -- Mathematics Dissertations -- Mathematics Theses -- Computer science Dissertations -- Computer science Software protection -- Mathematical models Computer security -- Case studies. Formal methods (Computer science) Mathematical Sciences Computer Science |
| url | http://hdl.handle.net/10019.1/2162 |
| work_keys_str_mv | AT seotsanyanamotlatsi formalspecificationandverificationofsafetyinterlocksystemsacomparativecasestudy |