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

applications. They may form the basis for harnessing theories for tool support
[17], a point we will return to in the concluding Section 4.related work.

Beyond Functional Aspects. In the more complex setting of objects or com-
ponents, the verification must go beyond pure functional properties as expressed
in the pre- post-condition paradigm. There is a state component as well that
enters in the post-condition and which satisfies some invariant .Furthermore,
many applications are reactive systems where the properties areprotocols,that
is constraints on behaviours of concurrent processes. An additional aspect occurs
with embedded systems where real-time properties are important. In Section 2
we will introduce suitable notation for expressing such non-functional aspects,
before we exemplify in Section 3 with conventional design patterns and extends
it with a discussion of timing properties which are important for embedded soft-
ware systems.

2 Background

In the following we introduce verification patterns more formally after defin-
ing the notations that are used to define properties. Settling on notation is a
matter of preference, but it is important that the chosen notation conveniently
can express what is required and that it is well established so that it is easily
understood. The most widely used notation for design patterns today is UML
[25] so UML class diagrams are the syntax in the following. To enable formal
specification and reasoning, the UML diagrams must be given semantics. The
formalism chosen to serve this purpose is the CSP-OZ-DC combination of Olden-
burg [12,21,20] as elaborated in Hoenicke's dissertation [13]. The CSP [10] part
hereof allows specification of processes, Object Z (OZ) [26] allows specification of
functional aspects for operations on objects, and Duration Calculus (DC) [31,30]
enables reasoning about time aspects.

OZ. Here, we are not going to go into syntactical and semantical details of OZ,
but just note that a class C corresponds to a Z schema, a method m to an
operation on the schema, and that an object o of the class C is a reference to a
value of the schema.

CSP. The communication events are elaborated such that a channel is associ-
ated with each public method and thereby with the corresponding schema oper-
ation. A method call to an object, say with input parameter x , actual argument
e , and output parameter y of type T , is written o.m !( x == e )?( y : T ), cf. [13].
Otherwise, we have the usual syntax for CSP processes which syntactically are
added as constraints to OZ schemas, or in UML as constraints in a responsibility
part of a class or object. For convenience, we list the CSP operators:

P ::= STOP | SKIP | ce → P | P P | P P | P P | P ; P