  An important aspect of many particle accelerators is the constant evolution
and frequent configuration changes that are needed to perform the experiments
they are designed for. This often leads to the design of configurable software
that can absorb these changes and perform the required control and protection
actions. This design strategy minimizes the engineering and maintenance costs,
but it makes the software verification activities more challenging since safety
properties must be guaranteed for any of the possible configurations. Software
model checking is a popular automated verification technique in many
industries. This verification method explores all possible combinations of the
system model to guarantee its compliance with certain properties or
specification. This is a very appropriate technique for highly configurable
software, since there is usually an enormous amount of combinations to be
checked. This paper presents how PLCverif, a CERN model checking platform, has
been applied to a highly configurable Programmable Logic Controller (PLC)
program, the SPS Personnel Protection System (PPS). The benefits and challenges
of this verification approach are also discussed.
