Book Title: FORMAL METHODS FOR REAL-TIME COMPUTING
Editors: Constance Heitmeyer and Dino MandrioliISBN: 0-471-95835-2
Publisher: John Wiley & Sons Ltd
Series: Trends in Software
Chapter 1
This chapter defines real-time systems and illustrates them with a
number of small examples. It also discusses issues central to applying
formal methods in the development of real-time systems: the trade-offs
between operational and descriptive specifications, different levels of
formality that can be applied, and the requirements of formal methods
for building industrial-strength systems. To put the newer formal
methods into perspective, two methods widely used in practice to design
and analyze real-time systems, namely, structured analysis and
Statecharts, are reviewed. Several promising new techniques for
specifying and analyzing real-time systems are then summarized and
illustrated with examples. These include graphical notations, state
machine and logic-based models, process algebras, and analysis
techniques, such as model checking and deductive reasoning.
Chapter 2
This chapter illustrates the use of the Modechart specification language
and the MT toolset by using them in the specification and analysis of the
control rod system of a nuclear reactor. The specification language and an
associated logic, RTL, are introduced, as is a tool for building
specifications. Two approaches are then used to analyze the specification.
The Modechart simulator is used to exhibit individual behaviors of the system.
The Modechart verifier is used to verify global properties of the system.
Chapter 3
We propose "timed (finite) automata" to model the behavior of real-time
systems over time. Our definition provides a simple, and yet powerful,
way to annotate state-transition graphs with timing constraints using
finitely many real-valued clocks. A timed automaton accepts timed
words --- infinite sequences in which a real-valued time of occurrence
is associated with each symbol. We study timed automata from the
perspective of formal language theory: we consider closure properties,
decision problems, and subclasses. We discuss the application of this
theory to automatic verification of real-time requirements of
finite-state systems. Finally, we give an overview of the heuristics
employed by different tools to alleviate the computational complexity
of the verification algorithm.
Chapter 4
The use of the Lynch-Vaandrager timed automaton model is illustrated
with a solution to the Generalized Railroad Crossing problem. The
solution shows formally the correspondence between four system
descriptions: an axiomatic (i.e., descriptive) specification, an
operational specification represented in terms of timed automata, a
discrete system implementation, and a system implementation that works
with a continuous gate model. Several sample proofs are given. In the
development of the solution, a number of guidelines were applied.
These guidelines, which should prove useful in applying formal methods
to practical systems, are described and illustrated with examples.
Chapter 5
A coherent and mathematically well-founded approach to the design of
real-time and hybrid systems is presented. It covers requirements
analysis and specification, design of controlling automata satisfying
the requirements, and derivation of occam-like communicating programs
from these automata. The generalized railroad crossing illustrates the
approach. Requirements are analyzed within a conventional dynamic
systems model of a plant, where states are functions of the reals,
representing time. The requirements are specified in an
assumption-commitment style using the Duration Calculus, a real-time
interval logic. Controlling real-time automata are specified in the
same formalism by elementary constraints on the plant states for each
control state or phase. The Duration Calculus is used to verify that
the control design refines the requirements. The real-time automata
map smoothly to component descriptions in a systems design language
that uses timed trace assertions over state transition events to
constrain control flow. Components can under certain conditions be
transformed to occam-like communicating programs.
Chapter 6
We report on our ongoing research whose long-term goal is to build
methods and tools for developing industrial-strength real-time systems.
We describe two independent but coordinated approaches, one an
operational formalism based on Petri nets and the other a specification
language based on logic. Both formalisms are specially designed to deal
with time-critical aspects of real-time systems. We also describe our
prototype tools and our experience in applying the tools in industrial
projects. In the long term, we plan to integrate the two approaches so
that system structure is described formally by a Petri net, whereas
system properties are expressed and proved in the logic language. We
discuss the advantages of such a ``dual language'' approach and the
barriers to applying the approach to industrial projects in the short
term.
Chapter 7
This chapter describes a timed process algebra, called ACSR, which
supports time-consuming actions and instantaneous events. Actions
model the usage of shared resources and the passage of time, whereas
events allow synchronization between processes. To be able to specify
real-time systems accurately, ACSR supports static priorities that can
be used to arbitrate between actions competing for shared resources
and between events that are ready for synchronization. ACSR also
offers different notions of equivalence that can be used to verify
that two processes behave the same. ACSR is illustrated through the
specification and analysis of a scheduler example, as well as three
variants of the railroad crossing problem.
Chapter 8
In this chapter we emphasize human-oriented usage of formal
specifications, and insist that these be not only amenable to automated
analysis but also appealing to human intuition and understanding. We
concentrate on a specification style called `constraint-oriented',
which is meant to simplify the writing and reading of formal
descriptions by approximating, in some aspects, the style of informal
descriptions as expressed in natural language. The constraint-oriented
style has already been applied succesfully to specifications in
standard LOTOS; in this chapter we show how it naturally extends to the
specification of time-dependent behaviours in timed LOTOS. The
approach is illustrated by the Generalized Railroad Crossing example.
Chapter 9
The chapter presents the use of symbolic model checking for the
verification of real-time systems. This method automatically
determines whether a temporal logic specification is satisfied for a
finite state model. Symbolic techniques use a representation based on
binary decision diagrams, which allow extremely large state spaces to
be handled. Real-time logics have been introduced that allow the
expression of time-bounded properties. In addition, we have introduced
quantitative reasoning in the verification process. The algorithms
that we have developed produce quantitative information about a
real-time system, in addition to determining its correctness. This
information allows a more detailed analysis than possible with previous
methods. These techniques have been applied to the verification of a
number of real-world system, of which we present a few examples: an
aircraft controller, a robotics system, a medical monitoring system and
the PCI local bus. These examples demonstrate that the techniques are
able to verify complex, realistic systems.
Chapter 10
This chapter presents a comprehensive design methodology for
guaranteeing end-to-end requirements of real-time systems.
Applications are structured as a set of process components, connected
by asynchronous channels, in which the endpoints are the system's
external inputs and outputs. Timing constraints are then postulated
between these inputs and outputs; they express properties such as
end-to-end propagation delay, temporal input-sampling correlation, and
allowable separation times between updated output values. The
automated design method works as follows: First new tasks are created
to correlate related inputs. An optimization algorithm, whose
objective is to minimize CPU utilization, transforms the end-to-end
requirements into a set of intermediate rate constraints on the tasks.
If the algorithm fails to find a solution to the constraints, a
restructuring tool attempts to eliminate bottlenecks by transforming
the application. Then it is re-submitted to the assignment algorithm.
The final result is a schedulable set of fully periodic tasks that
collaboratively maintain the end-to-end constraints.
OVERVIEW
Reproduced with permission of John Wiley & Sons Limited
For more information about the book, contact Connie Heitmeyer
(scr@itd.nrl.navy.mil) or Dino Mandrioli (mandriol@elet.polimi.it).
"Formal methods for specifying and analyzing real-time systems:
An overview," Constance Heitmeyer (Naval Research Lab) and Dino Mandrioli (Politecnico di Milano)
"Specification and analysis of real-time systems: Modechart language
and toolset," Aloysius Mok, Douglas Stuart (Univ. of Texas), and Farnam Jahanian (Univ. of Michigan)
"Automata-theoretic verification of real-time systems," Rajiv Alur (AT&T Laboratories) and David Dill (Stanford Univ.)
"Formal verification of real-time systems using timed automata," Constance Heitmeyer (Naval Research Lab) and Nancy Lynch (MIT)
"Refining system requirements to program specifications," Ernst-Rüdiger Olderog, Anders P. Ravn, and Jens U. Skakkebæk
"A Petri net and logic approach to thespecification and analysis of
real-time systems," Dino Mandrioli, Angelo Morzenti, Mauro Pezzè, Pierluigi SanPietro, and Sergio Silva (Politecnico di Milano)
"A process algebraic approach and methodology to the specification and
analysis of resource-bound real-time systems," Insup Lee, Hanêne Ben-Abdallah, Jin-Young Choi, and Duncan Clarke (Univ. of Pennsylvania)
"Constraint-oriented specification style for time-dependent behaviors,"
Tommaso Bolognesi
"Analysis of real-time systems using symbolic techniques," Sergio Campos, Edmund Clarke, and Marius Minea (Carnegie-Mellon Univ.)
"End-to-end design of real-time systems," Richard Gerber, Seongsoo Hong, Dong-In Kang, and Manas Saksena
CHAPTERS' ORGANIZATION