Formal methods for real-time systems must address the following problems:
- Modelling:
- Select appropriate models and formal notations
for adequately describing plants and controllers. These notations must deal
with the dynamic and reactive nature of the plants, and allow for the proper
expression of timing properties.
- Verification:
- The verifier is presented with a formal mathematical model
SUD where
SUD = plant| controller, and a specification S of how the plant
should behave. The verification problem involves demonstrating that
SUD satisfies the specification S.
- Development:
- In controller development a specification S
is given that the plant must satisfy (the
controller is not given).
A disciplined method is sought whereby designers can be helped to
construct a
controller so that SUD satisfies S. In development the
controller should be built in a modularly structured compositional fashion
(``controller architecture'').
- Synthesis:
- If controller development is fully automated, then it is
called controller synthesis.
There are a few surveys in the literature of formal methods for real-time
systems design [60,22,133]. This survey uses syntactic categories
to classify the various formalisms. There are three main directions that must
be distinguished, arranged by increasing formality and hence abstractness of
approach. The first category to be dealt with is real-time languages. Then
formalisms with visual specification languages are treated. Finally logics and
algebras are discussed.