ASADAL/PROVER: A Toolset for Verifying Temporal Properties of Real-Time System Specifications in Statechart

摘要

Critical properties of real-time embedded sys- tems must be verified before these systems are deployed as failing to meet these properties may cause considerable property dam- ages and/or human casualties. Although Statechart is one of the most Popular languages for modeling behavior of real-time systems, proof systems [5], [9], [14] and analysis tools [1], [2] for Statechart so far are in research and do not fully support the se- mantics of the original Statechart [8], or have limited capabilities for proving real-time properties. This paper introduces a toolset ASADAL/PROVER for verifying temporal properties of Statechart extended with justice and compassion properties. ASADAL/PROVER is composed of two subsystems, RTTL-Prover and Model-Checker. The RTTL- Prover converts Statechart specifications into real-time tempo- ral logic (RTTL) formulas of Ostroff[18], [19], and then checks if the formulas satisfy a temporal property (also in RTTL) using theorem proving techniques. The Model-Checker supports veri- fication of a predefined set of real-time properties using a model checking technique. The RTTL-Prover can support verification of any real-time properties as long as they can be specified in RTTL and, therefore, messages generated by the tool are general and may not be of much help in debugging Statechart specifications. The Model-Checker, however, can provide detailed information for debugging. ASADAL/PROVER has been applied successfully to some experimental systems. One of on-going researches in this project is to apply the symbolic model-checking technique by [3] to sup- port Statecharts with a much larger global-state space. We are also extending the types of temporal properties supported by the Model-Checker.