Introduction

Critical systems are found in an increasing variety of application fields and industries like electronics, control, aeronautics, health equipment, etc. Most of them are embedded systems, controlling devices that may risk lives or damage assets, hence termed safety-critical systems. These applications generally involve concurrency and control aspects, as well as real-time requirements that challenge the development process. Building such applications requires advanced tools and techniques in order to support reliable and economically feasible development and verification processes.

Computer Aided Verification techniques, and particularly Modelchecking, constitute a promising approach that deals with these kinds of systems. These techniques have originally and mainly been applied to the automatic verification of circuits and protocols but their use is being extended to software intensive systems (e.g.[BCP+01], [AFM+02]). Moreover, formal models are being explored as a means to perform testing [JCTG96] and monitoring [HR01] of applications.

Providing user-friendly means for the description of formal requirements plays an important role in this technology transfer agenda (e.g. [DAC99, HM02]). A remarkable example is the pattern-based approach and catalogue of verification properties defined in [DAC99], which bridges the gap between natural language and verification logics, and also suggests that a large number of formal properties stated in practice fall into a small set of categories.

When developing VTS, our scenario-based notation, we focused on expressing real-time requirements in a visual and friendly fashion, avoiding the use of formal logics such as TCTL [ACD93], and the explicit use of observers, which may become in practice an overwhelming and error-prone task, even for practitioners trained in the use of formal methods.

The need for visual and simple formalisms (instead of powerful but often cumbersome logics) when dealing with event-based requirements has been pointed out in several works (e.g. [SHE01, HM02]). Specifying the whole expected behavior of a system, even in an abstract form, is usually a difficult task. We believe that the use of (partial) scenarios is a key strategy in dealing with the problem of expressing event-based properties. In particular, our approach consists in graphically describing those generic scenarios of the analyzed model which violate the requirements. A VTS scenario is basically an annotated partial order of relevant events which can be regarded as a pattern, in the sense that it denotes a (possibly infinite) set of matching executions.

VTS is meant to existentially predicate on scenarios. That is, it is used to state a simple but yet relevant family of questions of the form "Is there a potential run of the system that can match this generic scenario?". These questions are closely related to the concept of anti-scenario or forbidden scenario (e.g. [HM02, UKM02]) as we use them to express infringements of safety or progress requirements. These questions turn out to be decidable, and we have developed a tool to edit scenarios and model check them over timed automata models of the system under analysis.