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:
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)