A Symbolic Model Checker for Testing ASTRAL Real-Time Specifications

ASTRAL is a high-level formal specification language for real-time (infinite state) systems. It is provided with structuring mechanisms that allow one to build modularized specifications of complex real-time systems with layering. In this paper, the methods and techniques used in the prototype implementation of the ASTRAL symbolic model checker, which is a component of the ASTRAL Software Development Environment(SDE), are presented. The model checking procedure uses the Omega library to represent a subset of states, and model checking is carried out on the execution tree of an ASTRAL process. The tree is further trimmed by the execution graph of the process. The model checker combines both explicit state exploration and symbolic state calculation in order to reduce the number of variables needed by dynamically resolving their values as well as their histories along a path of execution. Based upon the ASTRAL proof theory, the model checker is modularized, in the sense that each time it...

• Type: Conference
• Year: 1999
• Where: RTCSA
• Authors: Zhe Dang, Richard A. Kemmerer
• Keywords: ASTRAL Specification, ASTRAL Symbolic Model, Embedded Systems, Model Checker, RTCSA 1999