VERIFYING PROPERTIES OF HMS MACHINE SPECIFICATIONS OF REAL-TIME SYSTEMS

A ''hierarchical multi-state (HMS) machine'' is an automaton in which multiple states may be true, multiple transitions may fire simultaneously, a state may be expanded into a lower-level HMS machine, and in which the transitions are ''controlled'' by predicates in a temporal interval logic called TIL. HMS machines provide a compact formalism for specifying and verifying the behavior of concurrent hard real-time systems. Two approaches to verification of properties of non-recursive HMS machines are presented: (1) an extension of tableau-based theorem proving that utilizes the logic TIL and the execution semantics of machines to verify safety properties, and (2) a variation of model checking that uses ''interacting'' parametric ''computation graphs.'' The first verification approach avoids the construction of a complete computation graph and the second approach permits the analysis of behavior of certain types of HMS machines using multiple, relatively simple computation graphs.