| Abstract |
We present an extension of the well known selection/resolution or simply model to include timing constrains. The model is a mathematical model for concurrent processes, where a complex system may be described as a set of coupled finite state machines. A feature which makes the model extremely attractive is that the coupling between machines is described in terms of predicates on communication signals. In many cases this helps to obtain brief, concise and understandable specifications. The model is a discrete linear time model with trace semantics. A calculus is defined on processes which may be composed using a synchronous or asynchronous product operation. The model contains acceptance conditions in order to express any desired -regular property of the system. Verification consists in proving trace inclusion. Our extension consists of the integration of an existing model of dense time based on COSPAN, a well-known verification tool for concurrent systems over discrete time. COSPAN HK89,KK86,HK90 is a software tool for the specification and the verification of coordinating systems, based on the model. COSPAN may be used to develop high-level specifications, analyze logical and stochastic behavior of a coordinating system and optionally produce very efficient C-code implementations directly derived from the high level specification. The tool employs a formal, hierarchical, top/down development procedure. Logical analysis in COSPAN is carried out through symbolic testing of the specified system against a user-defined behavior. The system is neither simulated nor executed, but a mathematical proof (or disproof) of the stated behavior is produced. Formal reduction techniques are used in COSPANs' analysis algorithms, to cope with the typically vast state spaces that are encountered in coordinating systems. In this work the model is extended to include real-time constraints. We use the concept of logical timers Di89 which are fictitious components used to keep track of the possible times at which events may occur. This way it is possible to exclude computation sequences that violate the timing assumptions. Thus a system that would violate a specification in a purely speed independent model might satisfy it under certain timing assumptions. COSPAN is extended by adding an on-the-fly automatically-generated ``monitor'' process which keeps track of timing constraints so as to exclude system behaviors that are inconsistent with the timing information. We present all the details about the implementation of the verification procedures for the timed process model build using COSPAN. The resulting new tool RTCOSPAN has been implemented without need to modify COSPAN's internal structure or the grammar, showing that dense time extensions of well designed verification tools are possible. RTCOSPAN is backwards compatible with COSPAN. We present the user-interface used to introduce the new features of RTCOSPAN, the design philosophy used to cope with the large state-spaces timers require, and provide enough details of the tool's internal data structures and algorithms. Finally we pinpoint certain bugs and limitations present in our current implementation. Our method is used for the specification and verification of two systems. The first example is an extension of the well known alternating--bit communication protocol which includes timing information, and the second example employs two parallel communication channels with arbitrary but finite transmission delays. To facilitate the reader our specifications are given in terms graphs instead of the RTCOSPAN specification language, since such a translation is straightforward. We have shown that COSPAN can be extended to handle bounded delay constraints in a natural manner, and that the resulting system can verify interesting example systems. The basic approach of separating the timing-independent and timing-dependent parts of the specification, and using the timer region construction for the timing-dependent part, can probably be applied to other verification methods, as well.
|
Επαλήθευση Συστήματος Πραγματικού Χρόνου - η Επέκταση του COSPAN σε Συνεχή Χρόνο
