See discussions, stats, and author profiles for this publication at: https://www.researchgate.

net/publication/270279486

Testing & verification of PLC code for process control

Conference Paper · October 2013

CITATIONS READS

11 9,517

3 authors, including:

Borja Fernández Adiego Enrique Blanco Viñuela

CERN CERN
29 PUBLICATIONS 266 CITATIONS 72 PUBLICATIONS 590 CITATIONS

SEE PROFILE SEE PROFILE

All content following this page was uploaded by Borja Fernández Adiego on 05 June 2015.

The user has requested enhancement of the downloaded file.

 THPPC080 Proceedings of ICALEPCS2013, San Francisco, CA, USA

TESTING & VERIFICATION OF PLC CODE FOR PROCESS CONTROL

B. Fernández, E. Blanco, A. Merezhin, CERN, Geneva, Switzerland

Abstract a manual tester [2]. These tests are a complement and

Functional testing of PLC programs has been historically not a replacement of the tests procedures done by hand,
a challenging task for control systems engineers. This indeed not all test are easily automated. The manual tester’s
paper presents the analysis of different mechanisms for analytic skills can hardly be replaced and these testers are
testing PLC programs developed within the UNICOS frequently needed in the interpretation of the test results.
(UNified Industrial COntrol System) framework. The Therefore manual and automated tests are not unrelated but
framework holds a library of objects, which are represented complement each other.
as Function Blocks in the PLC application. When a Formal methods, within this context, are mathematical
new object is added to the library or a correction of an techniques for the specification, development and veri-
existing one is required, exhaustive validation of the PLC fication of software and hardware systems. Applied to
code is needed. Testing and formal verification are two programming code, formal methods provide a precise
distinct approaches selected for eliminating failures of semantics of a program. Having this formalization we can
UNICOS objects. Testing is usually done manually or prove that the program is correct, meaning it meets the user
automatically by developing scripts at the supervision layer specifications. Considering that other testing mechanisms
using the real control infrastructure. Formal verification can never guarantee error-free applications this technique
proves the correctness of the system by checking whether appears to be a solution, however the complexity is an
a formal model of the system satisfies the properties or evident drawback.
requirements. The advantages and limitations of both The paper describes the environment where testing
approaches are presented and illustrated with a case study, procedures must be applied, the test methods employed
validating a specific UNICOS object. focusing basically in automated tests mechanisms and
formal methods. Finally a summary of results and analysis
INTRODUCTION of the advantages and disadvantages of applying these
mechanisms is depicted.
Nowadays any software functionality is required to be
delivered faster and with minimum cost while maintaining UNICOS PLC CONTROL SYSTEMS
the quality expected. This applies to any software and
also to process automation applications. These critical UNICOS is an object-based framework providing a
applications needs to be extensively tested to validate methodology and a set of tools to develop industrial control
the requirements and ensure a smooth execution 24/7 in systems. This framework is used in industrial installations,
industrial plants as manufacturing, nuclear plants, pharma, e.g. the LHC (Large Hadron Collider) cryogenic control
cooling systems, etc. systems, cooling and ventilation control systems, and the
Generally, it is accepted to divide tests according to their LHC vacuum control systems. This framework, which has
been developed at CERN over the past 10 years, contains
c 2014 CC-BY-3.0 and by the respective authors

level of specificity into: (1) unit testing, where a specific

section of code is tested separately, (2) integration testing, several packages, according to the kind of control system to
where all individual units are put together to be checked be developed. The UNICOS-CPC package [3] is devoted
globally and (3) system testing where the complete system to process control systems. The control systems studied in
is tested as a whole application. this paper are composed by two layers: the control layer
Currently, testing is applied to process control applica- based on PLC (Programmable Logic Controller), and the
tions as a black box tests of function blocks or modules supervision layer based on a SCADA (Supervisory Control
in combination with input simulations and visualization And Data Acquisition).
of the results by the manual tester. Test cases are
manually created from the requirements or specifications UNICOS Object Library
by the developer and basically testing is considered as In the framework, each physical device (e.g. valve)
another activity of development. Following the industrial and process units are modeled as UNICOS objects, the
automation standard ISA-62381 [1], process control appli- complete set of objects is called the Baseline library.
cations testing is done in two main stages: Factory and Each new object to be designed under the UNICOS
Site Acceptance Tests, FAT and SAT respectively. The framework must follow the UNICOS metamodel [4]. This
difference being whether the tests are performed in the metamodel defines a predefined structure with a naming
factory or in the real plant. convention, thus the interface of the new object is defined.
Copyright ○

Automated tests allow a better implementation of repeti- However the object functionality is not expressed and
tive or tedious duties and can be hardly accomplished by validated at this stage.
ISBN 978-3-95450-139-7
1258 Knowledge-based Techniques
 Proceedings of ICALEPCS2013, San Francisco, CA, USA THPPC080

This object library is composed by Function Blocks

in the PLC developed with the ST (Structured Text)
programming language from the IEC 61131-3 standard [5].
The specification of the objects functionality is currently
described in a non-formalized way. It consists in well-
structured documents where the developer describes the
object functionality. In addition, test catalogs describing
the behavior of some parts of the object have been created
for testing purposes.
Many authors have arrived to the conclusion that most
of the failures in a system are due to incomplete and
unambiguous requirements specification. Figure 1: Testing topology.
In UNICOS, an initial analysis of the functional require-
ments that we want to test and verify has been made. This and laconic though the execution time was rather long
analysis is the very first step to formalize and complete the and the maintenance has been found complicated. This
UNICOS objects specification. kind of automated testing can be classified as a system
testing according to the topology (see Fig. 1) and since
TESTING & FORMAL VERIFICATION the test script is at the supervision level. More appropriate
APPROACHES unit testing could be done by using proprietary simulator
tools thought this solution can be used independently of
Manual Testing & Automatic Testing the PLC platform (Siemens, Schneider or Codesys). The
The straightforward approach to test PLC programs is to developed test scripts contain a certain level of abstraction
do it manually using the supplier’s IDE connected to PLC. (implemented as test scenarios) allowing them to be reused
Within the UNICOS framework a PLC object is normally for different UNICOS object instances.
meant to have a supervision counterpart representation.
Having this in mind, another possible approach would Formal Verification
be using a SCADA application connected to the PLC.
A different approach is to apply formal verification to
Assuming the communication is correct, a tester can
the UNICOS-CPC baseline objects. Formal verification
manipulate devices and observe their reaction. Here, the
depends on the use of mathematically based techniques
good practice would be to have a test catalog with all
and tools for the design, development and analysis of
the test cases explicitly written. The tester can simply
systems. The reason of using formal methods is to try to
follow the instruction and mark performed tests with the
increase the level of correctness. Using testing approaches
corresponding results.
is usually impossible to test all the possible combinations,
The UNICOS Baseline has been developed containing
this problem can be solved by using formal verification and
different object parametrization. To complete the tests
bugs can be detected before the system is implemented.
additional PLC code has been programmed to test some
The general idea is to create a formal model of the
object features which require additional inputs and/or
real system and check its correctness against formal
variables (e.g. interlocks behavior). Table 1 shows a
requirements describing the expected behavior of the

c 2014 CC-BY-3.0 and by the respective authors

simplified example of test catalog for three UNICOS object
system. There are two different approaches of verification:
configurations which validates the behavior on temporal
axiomatic verification and algorithmic verification.
stop interlock (TS). The table’s header represents the
test sequence performed at SCADA layer. Each line Axiomatic verification is a formal method for verifying
represents expected states of the corresponding device the functional correctness of a structured sequential pro-
parametrization. The test script has been based on the test gram by tracing its state changes from an initial condition
catalog. to a final condition according to a set of rules. Theorem
Provers are the tools used for this kind of verification (e.g.
Coq theorem prover). It is really hard to automatize and
Table 1: Test Catalog Example: A Sequence the success of this technique depends also on the skills
Initial state TS goes on TS goes off of the engineers and researchers. It has been applied to
Config 1 off off off operating systems and compilers but also to PLC programs.
Config 2 on off on In [6], the Coq theorem prover is applied to formalize the
Config 3 100 0 100 semantics of the PLC languages described in the standard
IEC 61131-3.
The next evolutionary step was to automatize the tester’s Algorithmic verification is usually referred as model
routine. The SCADA programming language really fitted checking. This technique use semi-algorithms to check that
Copyright ○

this need, as its main purpose is to send an order and a global model (representing the whole system) meets the
retrieve a result. The test script appeared to be simple requirements. It is feasible to automatize the creation of
ISBN 978-3-95450-139-7
Knowledge-based Techniques 1259
 THPPC080 Proceedings of ICALEPCS2013, San Francisco, CA, USA

these model and some theoretical limitations are overcome

by using abstractions. It is applied mainly to hardware,
abstract software and systems models.
Most of the verification applied in industry is done using
algorithmic verification and this is the approach selected to
verify PLC program based on UNICOS. Applying model
checking to any system requires the formalization of the
system and also of the requirements (See Fig. 2):

1. Formalization of the system is done by creating mod-

els using formalisms as Petri nets, labelled transtion
systems, timed automata, hybrid automata, etc.

2. The requirements are usually formalized using tem-

poral logic. Temporal logic is a formalism to express
unambiguously the requirements or properties. It
contains a set of rules for representing propositions Figure 3: Transformation of ST PLC code to NuSMV input
qualified in terms of time. language through an automata based abstract model.

formal verification can be applied with NuSMV (as shown

in the figure) and other model checkers, like UPPAAL.
This methodology in being currently implemented in an
automatic generation tool based on EMF (Eclipse Model-
ing Framework) and Xtext, from ST we can produce formal
models for NuSMV, UPPAAL and the input language
of the BIP (Behaviour, Interaction, Priority) framework,
passing through the intermediate model. This approach
will provide a good test bench to compare performance
limitations and identify the more appropriate tool for the
kind of properties to verify.
Formal methods techniques can be applied also to
complete control systems developed with UNICOS. In the
Figure 2: Model checking approach. paper [10] we presented a first approach for formalizing
a complete UNICOS control system using the BIP frame-
There are a significative number of available model work.
checking tools available. Some of the most popular or
relevant are NuSMV, UPPAAL or SPIN.
ANALYSIS & EVALUATION OF THE
Model checking approaches for the verification of PLC APPROACHES
c 2014 CC-BY-3.0 and by the respective authors

programs have been studied before for different application PLC software development lacks of modern software
areas and description languages. The reference [7] applies engineering best practices such as unit test or daily builds.
algorithmic verification to the SFC language. Untimed Automated testing via SCADA is feasible and in certain
SFC models are transformed into the input language cases allows to save the time spend on testing. We
of the Cadence SMV tool. Timed SFC models are found examples where the test case can be shared between
transformed into timed automata and they can be analyzed different objects. We also reuse automated test scripts
by the UPPAAL tool. The reference [8] models and to test different types of PLC. Automatic testing permits
analyzes a safety-critical system using coloured Petri reducing human errors, though the approach has several
nets as formalism and symbolic model checking for the issues: (1) it involves many components (the systems must
analysis. In [9] they model and apply formal verification be operative and properly communicating) which makes
to a particular timed multitask PLC to a specific platform it hard to support and replicate; (2) it is not possible to
from the Bosch Group. test all possible combinations of parameters of a baseline
object; the cost of each parameter’s combination test is
Our Approach and Contribution For the verifi- relatively high; (3) it is a black box testing of PLC code
cation of UNICOS-CPC baseline objects, we propose - it is not possible to manipulate or observe the variables
a methodology for its formalization in automata based which are not communicated. Additional PLC code must
models for further treatment with verification tools (see also be implemented to simulate PLC events and inputs via
Copyright ○

Fig. 3). Baseline objects are formalized in a generic the supervision scripts.
intermediate model and then using another transformation Formal verification techniques are not widely used in
ISBN 978-3-95450-139-7
1260 Knowledge-based Techniques
 Proceedings of ICALEPCS2013, San Francisco, CA, USA THPPC080

Table 2: Overview of Automatic Testing and Formal Verification for UNICOS Baseline Objects
Advantages Disadvantages
Automatic Testing with the real system Sophisticated maintenance
Testing Technology is available High price for new test case
Reduce human errors Black box testing
Reusable for different PLC Difficult to find the source of the problem
Model Explores all the combinations Verification of a system model
Checking Earlier bug detection Need of automatic generation tools
Avoid human errors Need to prove the transformations
Complexity hidden by the generation tools State space explosion
Counter-examples to find the source problem Applying abstractions techniques is not trivial

industry because of the complexity of, both, building tool to produce models of our control systems and verify
the models of the PLC systems and formalizing the them with different model checkers is under development.
specifications. Control system engineers are usually not A mathematical proof of the transformations rules (se-
familiar with these techniques, rising the need of automatic mantics preservation) is required as providing a formalism
generation tools to hide this complexity. Another common to specify unambiguously the test catalog, hiding the
problem in formal verification is the state explosion complexity of temporal logic for control engineers.
problem. As an example, trying to verify UNICOS-CPC
objects with about 750 lines of ST code and about 120 REFERENCES
variables, integers or float, causes some severe issues with [1] ANSI/ISA 62381: Factory Acceptance Test (FAT), Site
the performance of the model checker. However, providing Acceptance Test (SAT), and Site Integration Test (SIT),
(1) automatic generation tools for the models, (2) a good Automation Systems in the Process Industry.
language to express properties, and (3) the right technique [2] E. Dustin, T. Garrett, B. Gauf. Implementing Automated
for abstraction, model checking can be an useful and Software Testing: How to Save Time and Lower Costs
powerful technique to verify PLC control programs. Model While Raising Quality”. Addison-Wesley Professional,
checkers provide counter-examples, when the model does March 2009.
not reach a specification property. This feature definitely [3] E. Blanco et al. UNICOS Evolution: CPC version 6,
helps the developer to find the original problem. ICALEPCS, Grenoble (France), 2011.
Table 2 summarizes some of the advantages and disad- [4] B. Copy et al. Model Oriented Application Generation for
vantages of both approaches. Industrial Control Systems, ICALEPCS, Grenoble (France),
2011.
CONCLUSIONS AND FUTURE WORK [5] IEC 61131: Programming languages for programmable
This paper present an analysis of two different tech- logic controllers, International Electrotechnical Commis-
niques aimed to test and verification PLC control systems, sion.
specifically applied to UNICOS-CPC baseline objects. [6] J. O. Blech and S. O. Biha. Verification of PLC Properties
Automatic testing and formal verification approaches are Based on Formal Semantics in Coq, 9th SEFM, Montevideo

c 2014 CC-BY-3.0 and by the respective authors

meant to guarantee that the PLC control systems meet the (Uruguay), 2011.
specification requirements. Both techniques have different [7] N. Bauer, S. Engell, R. Huuck, B. Lukoschus, and
advantages and disadvantages but they can complement O. Stursberg. Verification of PLC programs given
each other. While automatic testing seems a more as sequential function charts. Integration of Software
feasible technique to implement, formal verification seems Specification Techniques for Applications in Eng., Springer,
a powerful future option. LNCS, 2004.
Ideally formal verification could be integrated in the [8] T. Bartha et al. Verification of an Industrial Safety Function
development process of PLC control systems, in our using Coloured Petri Nets and Model Checking, 14th MITIP
case inside the UNICOS framework. This will help the 2012.
control engineers to detect and correct bugs before the [9] H. B. Mokadem et al. Verification of a Timed Multitask
PLC application is deployed. Once this verification step System with UPPAAL, IEEE Transactions on Automations
is finished, automatic testing could be applied within the Science and Engineering 7, 4(2010) 921-932.
real PLC control system, then bugs can be detected if any [10] B. Fernández et al. Model-based Automated Testing of
situation was not taken into account on the formal models. Critical PLC Programs.11th INDIN. Bochum (Germany),
Next work on automatic testing will focus on extending 29-31 July 2013.
the test coverage and also performance improvement when
making the tests.
Copyright ○

Concerning formal verification, an automatic generation

ISBN 978-3-95450-139-7
Knowledge-based Techniques 1261