Property Patterns for the Formal

Verication of Automated Production

Systems

Jose Creissac Campos

Jose Machado

Eurico Seabra

Departamento de Informatica/CCTC, Universidade do Minho,

Braga, Portugal, (e-mail: [email protected]).

Departamento de Engenharia Mecanica, Universidade do Minho,

Guimaraes, Portugal, (e-mail: {jmachado,eseabra}@dem.uminho.pt)
Abstract: In recent years, several approaches to the analysis of automation systems depend-
ability through the application of formal verication techniques have been proposed. Much of
the research has been concerned with the modelling languages used, and how best to express the
automation systems, so that automated verication might be possible. Less attention, however,
has been devoted to the process of writing properties that accurately capture the requirements
that need verication. This is however a crucial aspect of the verication process. Writing
appropriate properties, in a logic suitable for verication, is a skilful process, and indeed there
have been reports of properties being wrongly expressed. In this paper we put forward a tool
and a collection of property patterns that aim at providing help in this area.
Keywords: Analysis of reliability and safety, Methodologies and tools for analysis of
complexity, Modelling
1. INTRODUCTION
The reliability, availability, and maintainability of auto-
mated systems (i.e. its safe operation) have a direct impact
on people and goods safety. Guaranteeing the safe opera-
tion of a system requires an holistic approach to design,
that takes safety considerations into account from the early
design stages through to operational exploitation.
Formal verication of software is becoming established
as a useful and powerful technique for guaranteeing the
correctness of software artefacts in general. This is also
the case for industrial controllers analysis [Moon, 1994].
Formal Verications main advantage is that it enables
analysis of all possible system behaviour. Typical men-
tioned disadvantages relate to the time and computational
resources needed for the attainment of formal verication
results, and to the level of expertise needed to apply the
verication techniques. In this paper we address this latter
issue.
In recent years, several approaches to applying formal ver-
ication techniques on automation systems dependability
have been proposed. These range from formal verication
by theorem proving [Roussel and Denis, 2002] to formal
verication by model-checking [Smet and Rossi, 2002,
Rossi, 2003, Gaid et al., 2005, Machado et al., 2006].
As verication tools gain popularity, the problem arises
of making its use scale to more realistic settings. The

This work was carried out in the context of the SCAPS Project
supported by FCT, the Portuguese Foundation for Science and
Technology, and FEDER, the European regional development fund,
under contract POCI/EME/61425/2004, and which deals with safety
control of automated production systems.
scalability of such tools is aected by a number of factors,
from the scalability of the algorithms being used as the size
and complexity of the problems being faced increases, to
their proneness to human errors during the modelling and
interpretation of results phases as potential users become
less procient in the verication techniques being applied
under the hood. We refer to this latter aspect as the
accessibility of the verication tools.
We have been working on this issue of making verication
more accessible. In order to help the analysis of PLCs (Pro-
grammable Logic Controllers) programs, it is important to
facilitate the use of automated reasoning tools. This can
be done at several levels. Three are:
help in deducing the controller model;
help in writing properties for analysis;
help in analysing the results.
One specic aspect that deserves attention is the writing
of properties to be veried. Meaningful properties can
be hard to write and hard to get right. This is even
more the case when we consider the behaviour of complex
automated systems, whose requirements are dicult to
describe.
Writing a property for verication is a two step process:
(1) we must rst identify what the relevant properties of
a given system are,
(2) and then we must decide how to correctly express
them in the logic of the verication tool.
Step 1 is domain dependent, and largely relies on knowl-
edge about the specic system being designed/veried and
what its properties should be. Step 2 is a technical step. A
Proceedings of the 17th World Congress
The International Federation of Automatic Control
Seoul, Korea, July 6-11, 2008
978-1-1234-7890-2/08/$20.00 2008 IFAC 5107 10.3182/20080706-5-KR-1001.4192
correct understanding of the model, the requirement, and
the logic in which properties are expressed is needed in
order to guarantee that the property being tested correctly
encodes the intent of the testing process. This is not a
trivial step. In [Dwyer et al., 1998] an example is reported
where a property was wrongly expressed. The process is
made more complex when the models are developed in
such a way that verication must only be performed at
certain specic points in the evolution of the system (for
example, because not all states in the model represent
stable system states).
In this paper we look at how the process of expressing
properties can be supported. Our approach is to provide
designers with patterns that can be instantiated to pro-
duce properties of interest. A tool is being developed to
support the approach.
The paper is structured as follows:
Section 2 describes our approach to modelling, and
the impact it has on how properties must be ex-
pressed;
Section 3 discusses property patterns, and in partic-
ular those proposed by [Dwyer et al., 1998];
Section 4 presents the tool we are developing to
support the use of patterns;
Section 5 presents a study of automation related
properties;
Section 6 introduces a new pattern collection for auto-
mated production systems verication that resulted
from the study;
nally, in Section 7 we discuss the results that have
been achieved and put forward lines for further work.
2. MODELLING APPROACH
Model-checking techniques [Berard et al., 1999] have been
employed for the formal verication of DES (Discrete
Event Systems) automation for the past twelve years.
A nite state system can be represented by a labelled
state transition graph, where labels of a state are the
values of atomic propositions in that state (for example
the values of the latches). Properties about the system
are expressed as formulae in temporal logic of which the
state transition system is to be a model. Model-checking
consists of traversing the graph of the transition system
and of verifying that it satises the formula representing
the property, i.e., the system is a model of the property.
As part of a dependable controller design approach, the
target verication system model may comprise [Frey and
Litz, 2000] either the controller on its own, assumed to
be placed in an open-loop on the plant (non model-based
verication) or the controller + plant set interacting within
a closed-loop (model-based verication).
Both in the non model-based and model-based formal
verication there are some properties that can be sys-
tematically veried. For instance, some properties of the
controller model like safety and liveness properties, related
with the internal states of the controller program [Bornot
et al., 2000], can be deduced in a systematized way. Also,
some properties, related with the plant model, like safety,
liveness, and other properties related with the stability
of the plant model, can be expressed always in a sys-
tematized way. This concept of stability is related with
states of the plant model that may not correspond to true
states of the plant behaviour. The concept of stability
associated at the plant model is well explained by Machado
et al. [2006].
By studying and identifying the properties used for the
verication of DES automation, it becomes possible to
systematize the writing of such properties in an automatic
way. That is the goal of this work.
3. PROPERTY SPECIFICATION PATTERNS
A number of classications for property specications in
the context of model checking approaches have been pro-
posed. Manna and Pnueli [1991] used a syntactic approach,
proposing a taxonomy of LTL (Linear Time Logic) for-
mulae. The taxonomy is based on the operators used in
each formula, therefore it covers all possible specications
that can be expressed in the logic. The categories they
dene, however, tend to be rather broad, and came from a
theoretical perspective. While they can be useful to classify
existing specications, they provide little support for the
process of generating new specications.
In [Manna and Pnueli, 1990] the same authors had pro-
posed a more pragmatic approach, a proof system that
handles three basic types of properties: invariance (ex-
pressing that something holds in all states of the system
for example, the liquid in a tank will always remain
below a predened maximum value); response (expressing
cause-eect relations for example, if the tank becomes
full the output valve will be open); and precedence (ex-
pressing something must happen before something else
for example, before the valve is closed, the tank must be
empty).
Dwyer et al. [1998] propose a more elaborate system
of patterns. They carried out an extensive review of
published property specications, and identied recurring
patterns which they organised into an hierarchy.
The term design pattern was rst introduced by Gamma
et al. [1995] as a means of capturing and transmitting
experts knowledge in the eld of object-oriented design.
A pattern is not simply a mechanism to classify some
artefact (be it a object-oriented design, or a property
specication) into a category. A patterns goal is to capture
proven solutions to known problems, and demonstrate how
they can be used in practice to solve the same or similar
problems in new situations.
With the above in mind, Dwyer et al. [1998] provide, for
each pattern, a description that includes the patterns
intent, examples and known uses, relationships to other
patterns, and mappings to dierent logics (in particular,
LTL and CTL Computational Tree Logic [Clarke et al.,
1986]). Additionally, the patterns can be tailored with
scopes: they can be applied to the whole of the models
behaviour, or be restricted to work between specied
conditions.
A full account of all the patterns is out the scope of
this paper. Briey, three classes of patterns are identied:
occurrence (dealing with whether specic conditions are
veried in the behaviour of the system), order (dealing
17th IFAC World Congress (IFAC'08)
Seoul, Korea, July 6-11, 2008
5108
Fig. 1. The patterns tool
with the order in which events/conditions occur), and com-
pound (dealing with chains of events/conditions). Some of
the most relevant patterns are:
absence a given state/event (P) does not occur (in
CTL this is expressed as AG(P))
universality a given state/event (P) occurs always
(in CTL this is expressed as AG(P))
response a given state/event (P) must always be fol-
lowed by a state/event (Q) (in CTL this is expressed
as AG(P AF(Q)))
precedence a given state/event (P) always precedes
some state/event (Q) (in CTL this is expressed as
A[Q W P])
4. TOOL SUPPORT
In our own work on formal verication we have been
developing tools to tailor the verication process to specic
domains. We are particularly interested in making the
verication process as accessible as possible. This includes
shielding the person performing the verication from the
technicalities of the process as much as possible. Of course
this must be done without hindering the verication pro-
cess itself. While the patterns can be a useful tool, the
manual process of selecting and applying a pattern is error
prone, and such error can be hard to detect.
In order to address this, we decided to develop a tool to
help the generation of properties from the combination
of models and patterns. The tool (Properties Editor
see gure 1) is based on the notion of property patterns
described above. A list of property patterns and help
for instantiating those patterns with the attributes and
actions in the model are provided.
The patterns include all the information in the original
patterns, such as intention and known uses.
Instantiation of patterns to produce a property specica-
tion can be done in two modes: manual mode and auto-
matic mode. In manual mode, the values for the patterns
parameters are indicated manually by the users. In gure 1
the user has provided the value ev1 to parameter P, and
the value ac=1 to parameter Q. Since the pattern being
used is Response, the property being constructed states
that ac=1 is a response to ev1 (in CTL: AG(ev1
AF(ac=1))). In automatic mode, the system reads
the attributes from a model and the user can use pull
down menus to select which attributes are used in the
parameters. For each pattern, codications in CTL and
LTL are available. This way, the formulae are created in a
transparent manner.
As illustrated in gure 1 the tool supports both the
patterns in [Dwyer et al., 1998] (Dwyer), and the patterns
we will be introducing in section 6 (SCAPS). To this end,
a DTD for the description of patterns has been developed,
and support for reading pattern collections expressed in
XML, in accordance to that DTD, integrated into the tool.
5. A STUDY OF AUTOMATION RELATED
PROPERTIES
Patterns do not provide concrete solutions. Instead, they
provide templates that must be tailored for specic pur-
poses. Hence, when attempting to apply the patterns to a
specic area two questions arise:
On the one hand, the patterns should capture the
relevant knowledge for the specic area being con-
sidered. Is all the relevant knowledge (or, at least,
enough of the relevant knowledge) captured by the
current set of patterns being used?
On the other hand, the manner in which the proper-
ties are formulated should be adequate to the logics
and modelling approaches used in the area of interest.
Are the languages and encoding strategies used in the
patterns adequate?
In order to answer these two questions we carried out a
study of property specications in the area of automation
control (our area of interest in the current context).
The objective of the study was similar to that carried out
by Dwyer et al. [1998]: to collect properties used in the
literature, and look for possible patterns. The justication
to perform a new instance of a study of this type was
two fold: on the one hand the original study already had
a number of years, begging the question of whether new
patterns had arisen; on the other hand, we were interested
in a particular application of the verication technology,
and in determining whether domain specic patterns are
being used in that context.
A number of papers and theses was analysed. Space con-
straints prevent an exhaustive enumeration. Relevant ex-
amples are [Bornot et al., 2000, Yang et al., 2001b, Mertke
and Frey, 2001, Rossi, 2003, Zoubek, 2004]. In many
cases the papers concentrated mainly in the modelling
approaches, with little being said about the verication
itself. Consequently, in those cases little information was
provided about which properties were veried, and how
they came about. This reinforced our perception that work
is needed in this area.
17th IFAC World Congress (IFAC'08)
Seoul, Korea, July 6-11, 2008
5109
A total of 6 main case studies (plus a number of smaller
examples) was analysed, resulting in over 70 property
specications. These properties were then aggregated into
six classes according to their syntactical structure, and the
type of application. The six identied classes are (typical
formulations are introduced, they all are expressed LTL
except the rst and last that are in CTL):
(1) Possibility AG EF P, meaning P is always possi-
ble;
(2) Fairness G F P, meaning P occurs innitely often;
(3) Absence G (stable P) , meaning P does not
occur (in stable states);
(4) Response G (P F(stable Q)), meaning after
P, Q will happen (in a stable state);
(5) Universality G P, meaning P occurs in every
state;
(6) Precedence A[Q W P], meaning P always pre-
cedes Q (this pattern was very rare).
Comparing these classes back with the patterns dened
by Dwyer et al. [1998] we nd that four of the classes
corresponded to patterns in the patterns systems (3 to 6),
while two of them do not (1 and 2). However, even for the
patterns that have correspondence, the formulation of the
properties do not totally coincide.
Given the particular modelling approach used in the
eld, a considerable number of properties used special
variables to restrict the analysis to stable states. While
this can at rst seem a detail to be dealt with during
pattern instantiation, it has in fact a great impact on
the structure of the properties. The introduction of such
variables requires considerable knowledge of the logics
being used if it is to be done properly.
The conclusion, then, is that we should dene a new pat-
tern system best adapted to the area of automation. These
patterns should include the Possibility and Fairness pat-
terns, and provision for the consideration of stable states
(in a similar way as scope is already being considered).
6. A NEW PATTERN COLLECTION
In this section we describe the proposed patterns. For each
pattern we list its intent, its formulation in LTL and CTL
(when available), and some examples of use, as well as its
adaptation to consider stable states only. Where available,
examples of inappropriate use are also provided.
Throughout the descriptions P and Q will be used to
denote variables that need instantiation.
6.1 Possibility Pattern
This pattern was not present in the original pattern
collection used for the properties editor tool. Interestingly,
it was found to be one of the three most common patterns
in the literature. Whether this is a specicity of this area
is a question that needs further analysis.
Intent To express that some event or state is always
possible throughout the execution of the system. Note that
it does not require that the state or event actually happens
in a specic execution of the model, only that it is possible
that it will.
Basic formulation
CTL: AG EF P
P is always possible.
Stable formulation
CTL: AG EF (stableP)
P is always possible in a stable state.
Examples Rossi [2003] uses this pattern to express the
absence of dead code. The author writes a family of
properties
AG EF(etat = pre
i
)
where etat is a variable that captures the current state
of the system and pre
i
are the possible execution steps.
Hence, what each properties says is that a particular
execution step is always possible.
Bornot et al. [2000] use this pattern to express that
two events (s4 and sfc top s3.s8) have to synchronise
repeatedly.
AG EF(s4 sfc top s3.s8)
In fact, this is a mislead application of the pattern since
proving the property does not guarantee that the events
ever synchronise in any specic execution of the model (see
intent above and the next pattern).
6.2 Fairness Pattern
This is another pattern not present in the original pattern
collection by Dwyer et al. [1998]. Despite not being one of
the most used, it was used to express relevant properties.
Intent To express that some event or state is repeatedly
possible throughout the execution of the system. Unlike
the possibility pattern, this pattern does require that the
state or event actually happens in the execution of the
model.
Basic formulation
LTL: G F P
P happens repeatedly.
Stable formulation
LTL: G F (stableP)
P happens repeatedly in stable states.
Examples Rossi [2003] uses this pattern to express dead
lock freedom
G F fdc
where fdc represents the end of the processing cycle.
The objective is to expresses that the processing cycle
repeatedly ends. Note however, that a behaviour which
satises the above property is that where the system does
not leave the fdc condition. Hence, the verication should
be complemented with the analysis of the fairness of other
steps.
6.3 Absence Pattern
This was one of the most common patterns.
17th IFAC World Congress (IFAC'08)
Seoul, Korea, July 6-11, 2008
5110
Intent To express that some event or state is not present
throughout the execution of the system.
Basic formulation
CTL: AG (P)
LTL: G (P)
P is never possible.
Stable formulation
CTL: AG (stableP)
LTL: G (stableP)
P is never possible in a stable state.
Examples Yang et al. [2001b] use this pattern repeatedly
to express both that a tank should not become empty and
that it should not overow
AG(Lev = 0) AG(Lev = 6)
where Lev represents the Level of the tank.
Mertke and Frey [2001] use this pattern to express the
following functional requirement
While the pressure is above 6.1 bar, motor 1
should not be turned on and motor 2 should
not be turned on.
resulting in
AG(rdy plc (i1) (o1 o2))
where rdy plc plays the role of our stable variable, i1
represents the pressure condition, and o1 and o2 are the
states of the engines.
6.4 Response Pattern
This is another of the most commonly used patterns. A
point that must be decided upon is whether the response
must be immediate. Patterns will be provided for both the
case when the response does not need to be immediate, and
for the immediate case.
Intent To express that some event or state will always
lead (immediately, or at some point in the future) to
another event or state.
Basic formulation
CTL (immediately): AG (P AX Q)
LTL (immediately): G (P X Q)
CTL (eventually): AG (P AF Q)
LTL (eventually): G (P F Q)
P always leads to Q.
Stable formulation
CTL (immediately): AG (P A[stable U (stableQ)])
LTL (immediately): G (P (stable U (stableQ)))
CTL (eventually): AG (P AF (stableQ))
LTL (eventually): G (P F (stableQ))
P always lead to Q at some future stable state (or at the
next stable state, in the immediate case).
Note that, depending on the specic analysis being per-
formed, we might wish to state that P must also be
considered in a stable state only (Pstable).
Examples Yang et al. [2001b] use this pattern to express
that a pump should not carry on working when the level
of a tank is running low
AG(Lev < 2 AF(m2 vB v4))
where Lev again represents the Level of the tank, m2 is
the state of the pump, and vB and v4 are valves states. In
this case it is not being required that the level is measured
at a stable state.
Bornot et al. [2000] use this pattern to express that a
specic condition on the state of the system (active s6)
immediately leads to a transition, and not to another
(x y s7 s8).
AG((active s6) AX(x y s7 s8))
Rossi [2003] uses this pattern to express the system re-
sponds to signals
G(E STOP F(fdc (MR MP0 MP1)))
where fdc is our stable variable, E STOP is the signal, and
MR MP0 MP1 characterises the correct response
of the system. Note that, assuming stable will eventually
hold, F(stable b) is equivalent to F(stable b).
6.5 Universality Pattern
This is one of the patterns that was present in the original
patterns collection and could be observed in our review of
the literature.
Intent To express that some event or state occurs in
every state of the execution of the system. This pattern is
in eect the opposite of the absence pattern.
Basic formulation
CTL: AG P
LTL: G P
P is always true.
Stable formulation
CTL: AG (stable P)
LTL: G (stable P)
P is true in all stable states.
Examples Bornot et al. [2000] use this pattern to express
that two events always synchronise.
AG(s4 sfc top s3.s8)
where s4 and sfc top s3.s8 are the two event that should
always be synchronised.
Yang et al. [2001a] use this pattern to express that the
temperature of a reactor always stays inside a desirable
range
AG(reactor.TREA > 0 reactor.TREA < 6)
6.6 Precedence Pattern
Few instances of this pattern were found. However, be-
cause it was a pattern present in the original pattern
17th IFAC World Congress (IFAC'08)
Seoul, Korea, July 6-11, 2008
5111
system, the decision was taken of including it in this
collection.
Intent To express that some event or state must occur
before some other event or state. Conceptually this pattern
is the opposite of the response pattern.
The pattern uses the weak until operator. Because this
operator is not usually supported by verication tools, we
provide alternative formulations with the more standard
operators.
Basic formulation
CTL: A[ Q W P]
CTL (alternative): E[P U (QP)]
LTL: G Q W P
LTL (alternative): F(Q) (Q U (P Q))
P always precedes Q.
Stable formulation
CTL: A[ (stableQ) W (stableP)]
CTL (alternative): E[(stableP) U (stableQP)]
LTL: G (stableQ) W (stableP)
LTL (alternative):
F(stableQ) ((stableQ) U (stableP Q))
P always precedes Q in stable states.
Examples Rossi [2003] uses this pattern to express that
a drill motor should always be stopped (dp drill motor)
before a conveyor belt is started (dp conveyor motor)
G(dp conveyor motor W (dp drill motor))
7. CONCLUSIONS AND FUTURE WORK
In recent years, several approaches to applying formal ver-
ication techniques on automation systems dependability
have been proposed. As verication tools gain popularity,
the problem arises of making them more accessible.
In this paper we have looked at the issue of supporting
the expression of property specications. We have briey
introduced a tool that supports the use of specication
patterns for the generation of properties for verication.
A study was carried out of properties present in the auto-
mated production systems analysis literature. A collection
of patterns has been put forward as a result of this study,
and was described in the paper.
Future work includes continuing to collect data from the
verication literature, in order to further validate and
perfect the current set of patterns. Further improvements
on the tool include the possibility of applying patterns to
families of states/events. This would allow, for example,
to check the fairness of all events in a system by applying
the pattern to all events, instead of having to individually
apply the pattern to each event. There is the need also
to apply the tool to a number of case studies in order to
better assess its value in the verication process.
REFERENCES
B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit,
L. Petrucci, and P. Schnoebelen. Systems and Soft-
ware Verication: Model-Checking techniques and tools.
Springer, 1999.
S. Bornot, R. Huuck, B. Lukoschus, and Y. Lakhnech.
Verication of sequential function charts using SMV.
In International Conference on Parallel and Distributed
Processing Techniques and Applications (PDPTA 2000),
volume V, pages 29872993. CSREA Press, June 2000.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic
verication of nite-state concurrent systems using tem-
poral logic specications. ACM Transactions on Pro-
gramming Languages and Systems, 8(2):244263, 1986.
M.B. Dwyer, G.S. Avrunin, and J.C. Corbett. Patterns
in property specication for nite-state verication. In
B. Boehm, D. Garlan, and J. Kramer, editors, 21st
Intern. Conf. on Software Engineering (ICSE98), pages
411420. IEEE Computer Society Press, 1998.
G. Frey and L. Litz. Formal method in plc programming.
In Proc. IEEE Int. Conf. on Systems Man and Cyber-
netics, pages 24312436, 2000.
M. Gaid, B. Berard, and O. Smet. Verication of an
evaporator system with uppaal. European Journal of
Automated Systems, 39(9):10791098, 2005.
E. Gamma, R. Helm, R. Johnson, and J. Vlissides. De-
sign Patterns. Addison-Wesley Professional Computing
Series. Addison-Wesley, 1995.
J. Machado, B. Denis, and J.-J. Lesage. A generic
approach to build plant models for DES verication
purposes. In 8th International Workshop On Discrete
Event Systems (WODES06), pages 407412, July 2006.
Z. Manna and A. Pnueli. Tools and rules for the practicing
verier. Technical Report STAN-CS-90-1321, Stanford
University, July 1990.
Z. Manna and A. Pnueli. Temporal Verication of Reactive
Systems: Specication. Springer-Verlag, 1991.
T. Mertke and G. Frey. Formal verication of PLC-
programs generated from signal interpreted petri nets.
In Proceedings of the 2001 IEEE Systems, Man, and
Cybernetics Conference, pages 27002705. IEEE, 2001.
I. Moon. Modeling programmable logic controllers for logic
verication. IEEE Control Systems, 14(2):5359, 1994.
O. Rossi. Validation formelle de programmes ladder pour
automates programmables industriels. PhD thesis,

Ecole
Normale Superieure de Cachan, France, June 2003.
J-M. Roussel and B. Denis. Safety properties verication
of ladder diagram programs. Journal Europeen des
Systemes Automatises, 36:905917, 2002.
O. De Smet and O. Rossi. Verication of a controller for a
exible manufacturing line written in ladder diagram via
model-checking. In 21th American Control Conference,
ACC02, pages 41474152, Anchorage, USA, May 2002.
CDROM paper n.734.
S.H. Yang, O. Stursberg, P.W.H. Chung, and
S. Kowalewski. Automatic safety analysis of
computer-controlled plants. Computers and Chemical
Engineering, 25:913922, 2001a.
S.H. Yang, L.S. Tan, and C.H. He. Automatic verica-
tion of safety interlock systems for industrial processes.
Journal of Loss Prevention in the Process Industries, 14:
379386, 2001b.
Bohumr Zoubek. Automatic verication of temporal
and timed properties of control programs. PhD thesis,
School of Computing, The University of Birmingham,
September 2004.
17th IFAC World Congress (IFAC'08)
Seoul, Korea, July 6-11, 2008
5112