Abstract

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.