Formal Methods for the International Space Station ISS - Correct System Design: Recent Insights and Advances - page 372

program until model checking (in combination with compositional reasoning
and generic theories) becomes feasible.
{ For verication of new programming languages, it would only be necessary
to develop a new front-end for transformation into the formal language; the
abstraction library could remain unchanged, since it does not depend on
the programming language, but on the formal specication language and its
semantics only.
Design Patterns and Generic Theories. The concepts of re-usability advertised
by object orientation had a very slow start in the eighties: approaches such as
the Ada Generic Package were not very widely used in practice. However, today
these concepts have matured and most software designers seem to have gained
a better understanding of how to benet from re-usability; for example, it is
a natural thing to use class templates and other generic concepts when pro-
gramming in C++ or Java. Beyond generic class concepts, design patterns (that
is, parameterised collaborations representing a set of parameterised classiers,
relationships and behavioural specications) and frameworks (that is, patterns
usable in a specic application domain) are presently becoming more popu-
lar [1,10]. The notion of patterns shifts the focus from isolated objects and their
properties to re-usable architectures comprising families of cooperating objects.
Initially, generic classes and design patterns have been introduced with the
main intention to increase software development productivity. Today, there is
a growing interest in the verication aspects of classes and patterns: what are
the guaranteed correctness properties which result from using an instance of
a specic generic class or from deploying a certain design pattern? What will
be the impact of the design decisions on the verication and test eort needed
to ensure sucient correctness of the resulting system? We believe that the
correctness properties of design patterns will gradually become more important
than the properties of isolated classes, since \local errors" in isolated method
implementations are often less harmful and easier to x than errors related to
the cooperation between objects: xing problems of the latter kind often means
re-designing whole portions of the system.
While in the context of the Unied Modelling Language [1,2] design patterns
and frameworks have only been dened in an informal way, closer analysis shows
that they may be formally interpreted as generic theories in the context of for-
mal specication languages admitting generic specications. For example, the
cooperating multiplexer/concentrator processes analysed in the verication of
deadlock freedom for the FML sketched above form a design pattern dened by
this specic way of communication between processes. The generic theory used
to derive deadlock freedom in Theorem 1 is a correctness property valid for all
instantiations of this design pattern.
We believe that the eciency of (formal) verication may be considerably
increased by providing \handbooks" of formally specied design patterns and
associated generic theories 10 : system designers might pick pre-dened patterns
10 A good example of the \handbook style" we have in mind is given by the generic con-
stants and associated mathematical laws of the Z Mathematical Tool-kit as dened