| dc.description.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. | |
