MultiVue: A multi-lingual specification and verification environment for real-time systems

Real-time systems have found a very wide range of applications from avionic systems, control systems for plants, patient-monitoring systems, military command and control systems, to control systems in automobiles, to name a few. Most of these systems are safety and time critical. Failures in these systems may cause catastrophic results in life and property. Therefore, it is extremely important to have the ability to formally specify and verify these systems, especially their timing properties.;In the past years, researchers have proposed many state-of-art formal methods for real-time system specification and verification. However, few have taken the approach of combining different methods to meet the challenges of today's complex real-time system design.;This thesis presents a multi-lingual environment, MultiVue, that integrates different specification and verification techniques into a unified framework. The key contribution is a multi-lingual architecture based on RTL*, which is a real time logic and specification language extended from Real Time Logic (RTL), and ModeFrame, which is a system structure specification language evolved from Modechart. ModeFrame views a system as a hierarchy of interacting modes. Its formal semantics is given in RTL*. A new specification language can be integrated to the environment by establishing a mapping protocol from timing related objects in the languages to events and modes in RTL* and ModeFrame. Timing verification and analysis tools associated with the particular language can be integrated into the environment through a tool-specific interface (TSI) based on the mapping protocol.;The thesis also presents several important contributions to the individual specification languages and verification tools in the environment.;Firstly, several subclasses of RTL* are identified as a means to manage RTL* verification complexity. For each subclass, either a set of high level inference rules is proposed, or a verification/analysis procedure is associated. Furthermore, a PVS based theorem prover is developed for reasoning about RTL* timing properties in a hierarchical way.;Secondly, a language called ModeTrans is proposed for specifying mode transitions. The axiomatic semantics of the language is formalized in RTL*. Modechart is redefined in a modularized way using ModeFrame and ModeTrans. Several new algorithms are devised for the modechart verifier to deal with arbitrary mode hierarchies and to significantly improve the time and space efficiencies in building the computation graph for a modechart. The reduced graphs also lead to more efficient verifications. Furthermore, a real-time symbolic model checker based on Ordered Binary Decision Diagram (OBDD) is developed for checking Temporal RTL (TRTL) against Modechart. One of the innovations in the model checker is an efficient algorithm for building OBDD's representing integer linear constraints, which are used to model clocks and event occurrences.;Thirdly, a novel approach is proposed to use TRTL as a springboard to enable hierarchical verification involving serial modes, and to build monitors for modeling many interesting RTL time properties using abstracted mode transitions.;Finally, an OBDD-based symbolic algorithm is developed to compute the min-max delays between the I/O's of a combinational hardware as a part of the effort to integrate hardware timing verification/analysis into the multi-lingual environment.