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

Design Verification Patterns

John Knudsen, Anders P. Ravn, and Arne Skou

Department of Computer Science
Aalborg University
Fredrik Bajers Vej 7E
DK-9220 Aalborg, Denmark
[e-mail]

Abstract. Design Verification Patterns are formal specifications that
define the semantics of design patterns. For each design pattern, the cor-
responding verification pattern give a set of proof obligations. They must
be discharged for a correct implementation of the pattern. Additionally
there is a set of properties that may be used in the design and verification
of applications that employ the pattern. The concept is illustrated by ex-
amples from general software engineering and more specialised properties
for embedded software.

1 Introduction

Engineers design; thus software engineering is a discipline that systematizes
knowledge about procedures for designing software. This is evident from the
structure of Dines Bjørner's volume on the subject [2]: After a careful analy-
sis of the application domain and a systematic elicitation of requirements, the
remaining task is design with implementation. Like in any other engineering dis-
cipline software design is based on reuse of patterns and well known components.
However, unlike other disciplines, software engineering does not systematically
use the patterns and components to analyse properties of the resulting system.
Software is generally built without systematic analyses. Throughout the Pro-
CoS project [8,14] it was the ambition to improve on this state of affairs, and
through numerous case studies, we demonstrated that is was feasible, see for
instance [24,23].
Yet, application of formal techniques have not spread dramatically, and it is
rather clear that it is so dicult that it will remain a specialist activity even
with better integrated notations like those developed in Oldenburg [21,13] and
at UNU/IIST [9,16]. Perhaps a remark from control engineering colleagues helps
to clarify, how dicult it is to work rigorously from basics: ”Either you choose
aPIDcontrolleroryouhavetogetaPhD-controller.” Yet, we cannot expect
every engineer to have skills at a PhD level, therefore we must rely on standard
components that we know well, and where there are standard procedures for
tuning them and checking their properties . Design Verification Patterns is an
attempt at defining properties for the standard design patterns for software
engineering.