Applying verification methods to nonexhaustive verification of software/hardware systems
Marc C. W. Geilen, Dennis R. Dams, Jpm Jeroen Voeten · TU/e Research Portal · 1998
Abstract — In order to handle the increasing complexity of hardware / software designs, system level design methods are being used. These methods are directed to produce op-erational 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 specifica-tion model has a well-defined semantics, and the require-ments 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 sys-tem 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.