Pompeo, François (1999) A formal verification assistant for TROMLAB environment. Masters thesis, Concordia University.
Formal specifications have become a strong basis in the field of safety critical systems development. Safety, liveness and time bounded properties are characteristics of such systems where the need to secure their adequate implementation is very high. Formal verification of such properties is the research field of this thesis. It presents an automated tool that enables mechanized axiom extraction from real-time reactive systems. It is implemented within TROMLAB which is a development environment based on the Timed Reactive Object Model (TROM). The objective of this tool is to be used within the verification methodology of TROM as an automated assistant to facilitate time dependent property proving for model developers.
|Divisions:||Concordia University > Faculty of Engineering and Computer Science > Computer Science and Software Engineering|
|Item Type:||Thesis (Masters)|
|Pagination:||ix, 100 leaves : ill. ; 29 cm.|
|Degree Name:||Theses (M.Comp.Sc.)|
|Program:||Computer Science and Software Engineering|
|Thesis Supervisor(s):||Alagar, V. S.|
|Deposited By:||Concordia University Libraries|
|Deposited On:||27 Aug 2009 17:15|
|Last Modified:||08 Dec 2010 15:17|
Repository Staff Only: item control page