Applying verification methods to nonexhaustive verification of software/hardware systems

In order to handle the increasing complexity of hardware / software designs, system level design methods are being used. These methods are directed to produce operational system models at a high level of abstraction. They can be used to assess early in the design phase if specific functional or performance requirements can be met. Since the systems that are being designed are often concurrent and real-time, the behaviour of these models can become rather complex. It is not always easy to check whether a model indeed satisfies the desired requirements. If the specification model has a well-defined semantics, and the requirements can be expressed exactly, it is possible to automate some of these checks. Several techniques exist to verify if a given model satisfies certain formally defined properties. A popular approach is model-checking, which is an automata based approach in which the verification problem is reduced to standard checks on finite state automata, as used in the tool Spin [1] for example. In this paper we investigate the use of such automata based verification techniques in simulation of high-level system specifications in POOSL [2]. We show how certain properties expressed in the formalism linear temporal logic (LTL), can be automatically monitored during simulations of complex distributed systems. Keywords--- formal verification, temporal logic, tableaux, simulation, object-oriented methods I.