Specification environment for distributed real time systems

Abstract

Real-time computer systems usually find applications in safety-critical areas. Thus, real-time systems need to be extremely reliable. However, most of the real-time systems are inherently "distributed" in nature. The increased complexity due to the "distribution" of system structure compounds the problem of developing reliable systems. It is widely acknowledged that use of formal specification techniques can contribute towards increasing system reliability. However, the existing specification techniques do not satisfactorily address to the issues of "distribution" and "real-time". In this context, this dissertation reports the work undertaken to develop a suitable specification environment for distributed real-time systems. This specification environment consists of two formal languages to describe the real-time behavior of systems at the requirements specification and system specification levels. A set of tools is also developed to reason about the specifications. The dissertation starts by examining the constraints imposed on specifications by the issues of "distribution" and "real-time". It turns out that new concepts concerning the underlying semantic model of formal specification languages are mandatory. Emphasis is placed on the need for a partial order framework due to the fact that global clocks are very difficult to implement in a distributed environment. For an accurate modelling of distributed real-time computations at different levels of abstraction, suitable semantic models are synthesized from the existing ones. Recent work has shown that complex systems like distributed real-time systems can be proficiently described, modelled, constructed, and managed in terms of their configuration. The underlying model associated with this configuration paradigm is a set o f processing components loosely connected by communi9ation channels. We advocate the use of the same underlying configuration throughout the system development activity and reflect the same in our two developed specification languages. The developed requirements specification language (TES) is based on a timed version of the event structures formalism. We have developed this timed version of the event structure formalism by timing event occurrences, and by associating a timing component with the causality relation. A language shell (named SLATES) for the timed version of the event structure is developed to provide convenient notations for easy construction of requirements specifications. To reason about requirements specifications, a modal logic (named TESL) patterned after the timed version of the event structures is developed. A method is provided for mechanical translation of the S L A T E S specifications into TE SL formulas. The problem of automatic verification of T E S L specifications is discussed and effective solutions are provided by extending the classical tableau algorithm. Automatic tools are developed to verify a restricted class of T E SL specifications. These developed tools include one for TESL model checking, another tool for checking the satisfiability (consistency) of TESL specifications and one more tool for checking the conformance of event traces with the corresponding specifications. To reason about unrestricted TESL specifications, a sound axiomatic system is developed. A modal logic called distributed logic (DL) is developed for system specification. D L is formulated as a first-order logic augmented with spatial modal and temporal operators. D L can be used to specify the real-time behavior of a distributed system with respect to an underlying system configuration. D L can provide an accurate model of real-time computations by defining a partial order among the states of an ordered set of total order state sequences. The total order state sequences represent computations of the individual nodes and the partial order relation allows us to combine the behavior of the individual nodes to arrive at some global properties of the system. A sound axiomatic system is developed to reason about xml restricted DL specifications. A set of tools is developed to automatically verify a restricted class of DL specifications. These automatic verification tools include one to check D L models, one to assess the satisfiability of D L specifications, and one more tool to test the conformance of event traces with the corresponding D L specifications. The developed framework has been tested on a number o f sample problems. The aim of such experiments is to demonstrate the adequacy o f the proposed specification languages and the effectiveness of the developed tools.