Design Verification Patterns - Formal Methods and Hybrid Real-Time Systems - page 411

3.3 Summary

We have illustrated that it is feasible to specify both functional, behavioural and
timing conditions that form design verification patterns. A few other patterns
have been investigated and give similar reasonably succinct conditions. Yet, there
is much more work to do. Some particularly interesting questions are to what
extent the verification patterns can be made complete for a given design pattern,
that is they give a precise characterization of the pattern. For the functional and
behavioural properties, we think they can be made complete, however, we are
not sure that that can be done for the timing properties, because these are
dependent on the underlying execution platforms.

4Con lu on

We have developed the concept of a verification pattern, the semantic twin to
syntactic design patterns. They are based on conventional rely-guarantee con-
ditions for an implementation which are used as assert-assume lemmas for the
application that uses them. The concept has been illustrated with functional,
behavioural and timing specifications for conventional patterns.

Discussion. The application of Design Patterns in practical design of embed-
ded systems is still at a early stage but as the complexity increase and the object
oriented paradigm gains ground in this field, so will the application of technolo-
gies known from this field. A substantial part of the research in Design Patterns
has focus on ecient solutions to architectural design challenges, and although
designers of embedded systems are faced with such challenges also, more ef-
fort on researching Design Patterns for the special challenges that characterise
embedded systems is needed.
In a case study of control software for marine diesel engines, that spurred our
research of Verification Design Patterns, we encountered behavioral challenges
typically encountered in control engineering that could be candidates for Design
Patterns and Verification Design Patterns in embedded software systems.
One such challenge was the modelling of the JetAssist , a system that assist a
turbo charger in optimizing the the fuel consumption and reduce CO 2 emission
levels. For the JetAssist the specification explicitly stated that the system should
have a hysteresis behaviour, i.e. the behavior of the system must by increasing
and decreasing temperature, in respective overlapping intervals displaying differ-
ent temperatures. That is, by measuring the temperature alone, is is not possible
to predict the behavior of the JetAssist. Hysteresis is known from a variety of
control and processing systems. Around this hysteresis pattern we found a num-
ber of well-known conventional patterns, exemplified by those described in this
paper. It was clear to us that if we are to prove proerties of the JetAssist in a way
that is comprehensible to engineers, we would have to structure the arguments
- thus the patterns.