A Method for Verifying Properties of Modechart Specifications.

Abstract

As software control of time-critical functions in embedded systems becomes more common, a means for the precise specification of their behavior becomes increasingly important. Modechart is a graphical specification language introduced to meet this need. This paper presents a method for verifying properties of systems specified in Modechart. The proposed approach makes use of a computation graph which takes advantage of the structuring inherent in a Modechart specification. Two classes of properties are presented for which decision procedures are developed. 1. Introduction Modechart is a graphical specification language developed to provide a compact and structured way to represent real-time systems [Jahanian & Mok 88]. Although similar in some ways to Harel's Statecharts [Harel 86], Modechart is specifically tailored to representing time-critical systems. The semantics of Modechart is given in Real Time Logic (RTL), a logic for the specification and analysis of such systems [Jahanian ...