Monitoring, testing, and abstractions of real -time specifications.

Abstract

As real-time and safety-critical computer systems become more prevalent, increasing attention has been paid to the use of formal methods in the specification, validation, and verification of such systems. However, many techniques for analyzing and verifying real-time systems have not scaled well to real-life applications. This dissertation presents three analysis techniques which reduce the state-space and refine the portion of the state-space which is searched during specification analysis. These three techniques, <italic>selection, truncation, and abstraction</italic>, form the basis for a more focused examination of specification behavior. Monitoring modules describe a property that the system should satisfy. When they are used in the context of simulation, they provide a mechanism for evaluating properties of the system on a particular computation prefix. When used in the context of verification,<italic> reachability-based model-checking </italic> can be performed. This permits the generation of the state-space to be terminated upon satisfaction or violation of a property. Controller modules specify constraints which control which part of the state-space is to be examined by limiting the range of input events. When used in the context of simulation, they perform powerful steering of the simulation. When used in the context of verification, they permit verification of a subset of the state-space. MTSim is an extensible, customizable simulation platform for Modechart specifications, which supports examination of individual computation prefixes. Simulation-verification synthesizes simulation and verification to achieve an intermediate analysis method which is an application of the techniques of selection and truncation. This method uses simulation to limit generation of a computation graph to the set of computations consistent with the simulation. Abstraction relations between Modechart modules make it possible to determine when one specification <italic>implements</italic> another, i.e. when they have the same set of computations. Several abstraction relations are described and compared. A new representation of the semantics of a specification is introduced. This representation, <italic>min-max</italic> automata, is more compact than other types of finite state automata typically used to represent real-time systems, since each path can represent more than one computation. In addition, automatic generation of abstraction modules is described using a <italic>dependency marking</italic> approach.