The work presented in this thesis is a part of a long term research
program which explores the application of rewriting logic
to the *executable formal modeling * of computing systems. The
general conceptual advantage of using a logic instead of using a
specific model is that many different models can be specified in the
same logic, each in its own terms, rather than by means of possibly
awkward translations into a fixed model. Since rewriting is executable,
and is supported by implementations of the rewriting logic
languages Maude, ELAN, and CafeOBJ.
these models can be formally analyzed using a flexible range of formal
analysis techniques including rapid prototyping, model checking, and
symbolic simulation.

The advantages of using rewriting logic as a semantic framework for concurrent systems, in which a wide range of concurrent system models can naturally be represented, has been amply demonstrated. On the pragmatic level, rewriting logic---due to its being based on a fairly natural and well-known formalism, its integration of static and dynamic system aspects, its abstract modeling of communication and concurrency, its support for concurrent object-oriented programming, and its possibilities of allowing user-defined execution strategies in the logic itself---has been shown to be an appealing formalism in which to specify and analyze a variety of applications such as communication and security protocols, which are complex enough to warrant prototyping and formal analysis, and whose operational nature fits very well with rewriting logic.

This thesis investigates whether rewriting logic is similarly
well-suited to model and analyze real-time and hybrid systems.
The first important research contribution exploring the application of
rewriting logic to real-time specification has been the work of Kosiuczenko
and Wirsing on *timed rewriting logic * (TRL), an
extension of rewriting logic where the rewrite relation is labeled with time
stamps. Although TRL has been shown to be adequate for specifying
a variety of
complex real-time systems,
it suffers from having rigid synchrony requirements and from changing
the logic, so that TRL specifications cannot be directly executed in a
rewriting logic language implementation.

Our work indicates that rewriting logic is indeed well-suited to model
and analyze real-time and hybrid system without having to change the
inference rules of the logic. We show how a wide range of models of
real-time and
hybrid systems, including timed automata, hybrid
automata,
timed and phase transition systems, timed extensions of
Petri nets, and
object-oriented real-time systems, can indeed be expressed in
rewriting logic quite naturally and directly as *real-time rewrite
theories *. Such theories are rewrite theories where real-time aspects are
highlighted. However, real-time rewrite theories are easily
reducible to ordinary rewrite
theories.

Thus, rewriting logic can be used to specify many different formal models of such systems in a unified logic. But, since rewriting logic is executable, these models can be executed and can be formally analyzed in a variety of ways. This is in contrast to the most well-known formal methods tools for real-time and hybrid systems such as Kronos, STeP, and UPPAAL. These are model checking tools which require the user to specify both the system and the formal properties the system should satisfy. The tools then try to check whether the system satisfies a given abstract property. Besides having somewhat restrictive specification languages for purposes of remaining as much as possible in decidable fragments, these tools are not well suited for directly executing the system itself. The same can be said about HyTech, which takes a hybrid system description with some parameters unspecified, and returns the concrete values of the parameters which would make the system satisfy some given property. Of course, different tools have different important strengths of their own. The point is that executable specification methods and tools can complement those strengths in new ways.

To see how rewriting logic complements more abstract specification
formalisms such as
temporal logic as well as more concrete, automaton-based ones, one can think
of it as covering an *intermediate operational level *, that can
substantially help in
bridging the gap between more abstract, property-oriented, specifications and
actual implementations by providing:

- a precise mathematical model of the system against which more abstract specifications can be proved correct by means of inductive theorem proving, model checking, and other techniques;
- support for other useful techniques of automated or semi-automated formal reasoning and analysis at the rewriting logic and equational logic levels, such as coherence, confluence, and strategy-based formal analysis;
- support for executable specification, symbolic simulation, and a wide range of formal analyses;
- the possibility of generating correct implementations from specifications by theory transformations and code generation techniques.

Indeed, after showing that rewriting logic is a suitable semantic framework for real-time and hybrid systems, we investigate how well the specification and analysis methods of rewriting logic already known to work well for concurrent and distributed systems (see for example specialize to real-time and hybrid systems. For this purpose, we have defined and implemented the Real-Time Maude specification language and analysis tool. The Real-Time Maude language extends the Full Maude language to support the specification of real-time rewrite theories in timed modules and object-oriented timed modules. The Real-Time Maude tool supports a wide range of techniques for formally analyzing timed modules. Besides supporting Maude's default execution strategy, it provides special-purpose strategies for the symbolic simulation of timed modules, and additional rewrite strategies and search commands for model checking timed modules with respect to properties stated in a subset of real-time temporal logic. Furthermore the tool's strategy library can be easily extended to define new application-specific analysis strategies.

For building the Real-Time Maude tool, we used Maude as a formal
meta-tool, in which other tools---in this case
the Real-Time Maude
tool itself---can be represented and executed. Specifically, the
specification of Real-Time
Maude extends the specification of Full Maude, and makes extensive use
of Maude's *reflective * features. Besides accruing great saving
in implementation effort, the reflective design of the tool as an
extension of Full Maude also means that the Real-Time Maude
specification language inherits and extends the rich module algebra of
Full Maude, including parameterized modules, theories, views, module
expressions, and object-oriented modules, all of which are supported
for real-time specifications.

The usefulness of a specification language and a formal methodology is measured by how well different examples and applications can be expressed, and by how effectively the formal analysis methods can be used to uncover flaws, or indicate the absence of errors, in informal specifications. We have tested the Real-Time Maude specification language and analysis tool on a variety of real-time systems, including a method for solving scheduling problems presented in this thesis. The most important case study we have undertaken has been the specification and analysis of a sophisticated protocol suite for reliable and efficient multicast in active networks, namely, the AER/NCA suite of active network protocols, developed by S.K. Kasera, S. Bhattacharyya, M. Keaton, D. Kiwior, J. Kurose, D. Towsley, and S. Zabele, which combines adaptability, fault-tolerance, real-time, performance, and composability of protocol aspects, and therefore presents a challenging specification and analysis problem of a kind typically not included in formal methods treatments of protocols.

We have used the tool to specify all protocols in the AER/NCA suite, as well as their composition, in an object-oriented style which is naturally supported by Real-Time Maude. We then have used the Real-Time Maude tool to formally analyze the protocols and their composition by executing them using the tool's standard interpreter and by extending the strategy library to model check the specification with respect to relevant temporal logic properties. This process has uncovered many missing assumptions, ambiguities, and flaws in the original informal specification.

(BibTeX entry) (gzip'ed Postscript)

back home Formal Methods and Declarative Languages Laboratory Computer Science Laboratory, SRI International