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

be used either as test and verification of the component, or in a test driven
applicaition development process model as assert/assume pairs for verification,
monitoring or for developing tests.

2.2 Related Work

There is a rich literature on verification, and patterns are implicit in many proof
rules, yet the idea of combining architectural patterns with verification occurs, to
our knowledge for the first time in [4,5]. It develops application specific pattern
for collision avoidance. A somewhat similar idea is to develop refinement rules
or conditions for design patterns; this is explored in [18]. Finally we mention [27]
which approaches design patterns with the same mission to delimit the responsi-
bilities of the developer and define the rewards for the application programmer.
Their proposal for formalization, however, does not distinguish between aspects
and thus require coding behavioural properties as state invariants.

3 Patterns

We begin with one of the most used and most simple design patterns; the Single-
ton pattern. A good example of its application is the control module for a ship's
rudders. A modern ship is controlled from several stations, but it is essential
that the rudders have one and only one common interface, such that clients that
needs access to the rudders access the same software unit. If different clients
have or create their own representation of the rudders, the representations are
hard, if not impossible to keep consistent. A correct instantiation of a Singleton
pattern eliminates such behaviour.

3.1 Singleton Pattern

The intent of the Singleton pattern is to ensure that there can only be one
instance of the Singleton class and to provide global access to this instance [6].

Singleton
− instance

Singleton()
+ Instance()

Fig. 2. The Singleton pattern as an UML class diagram

Figure 2 shows the UML class diagram for the Singleton pattern. Note that
the instance attribute has a

−

prefix, indicating that it is private to the class,
i.e. only accessible through methods/operations of the class. For the Singleton
class a protected constructor operation, Singleton(), is given and the public
operation + Instance().