Certification of Safety-Critical, Software-Intensive Systems
EECS4312:
Software Engineering Requirements Fall 2019
CHEN-WEI WANG
Acknowledgement of Collaborators
McSCert, McMaster University, Canada
○ Alan Wassyng [ faculty, P.Eng. ] ○ Mark Lawford [ faculty, P.Eng. ] ○ Linna Pang [PhD student]
Software Engineering Laboratory, York University, Canada ○ Jonathan Ostroff [ faculty, P.Eng. ] ○ Simon Hudon [PhD student]
Nanyang Technological University, Singapore
○ Yang Liu [ faculty ]
Singapore University of Technology and Design, Singapore ○ Jun Sun [ faculty ]
3 of 37
● Led a $20M project (MAR.2008 to SEP.2016) of ORF-RE (Ontario Research Fund for Research Excellence) on the
[IBM] [Legacy Systems International Inc (LSI)] [General Motors (GM)] [Candu, OPG, SWI, Radiy/Sunport]
Certification of Safety-Critical Software-Intensive Systems
● Objectives:
○ Certify software through product-focused approaches
○ Develop methods, tools, and a repository of certified components ○ Use formal methods to provide evidence for certification
● Collaborating with U of Waterloo and York U (Toronto)
● Working with industry and regulators to improve software in:
○ Biomedical Devices ○ Financial Systems ○ Automotive
○ Nuclear
● My contribution: verification of function blocks defined in standards for components used in the nuclear power industry
2 of 37
McMaster Centre for Software Certification
Developing Safety-Critical Systems
Industrial standards in various domains list acceptance criteria for mission- or safety-critical systems that practitioners need to comply with: e.g.,
Aviation Domain: RTCA DO-178C “Software Considerations in Airborne Systems and Equipment Certification”
Nuclear Domain: IEEE 7-4.3.2 “Criteria for Digital Computers in Safety Systems of Nuclear Power Generating Stations”
Two important criteria are:
1. System requirements are precise and complete
2. System implementation conforms to the requirements
But how do we accomplish these criteria?
4 of 37
Professional Engineers: Code of Ethics
○ Code of Ethics is a basic guide for professional conduct and imposes duties on practitioners, with respect to society, employers, clients, colleagues (including employees and subordinates), the engineering profession and him or herself.
○ It is the duty of a practitioner to act at all times with,
1. fairness and loyalty to the practitioner’s associates, employers,
clients, subordinates and employees;
2. fidelity to public needs;
3. devotion to high ideals of personal honour and professional integrity;
4. knowledge of developments in the area of professional engineering
relevant to any services that are undertaken; and
5. competence in the performance of any professional engineering
services that are undertaken.
○ Consequence of misconduct?
● suspensionorterminationofprofessionallicenses
● civillawsuits 5 of 37
Source: PEO’s Code of Ethics
Verification: Building the Product Right?
○ Implementation built via reusable programming components. ○ Goal : Implementation Satisfies Intended Requirements
○ To verify this, we formalize them as a system model and a set of
(real-time) properties, using the specification language of a
model checker or a theorem prover. ○ Two Verification Issues:
1. Library components may not behave as intended.
2. Successful checks/proofs ensure that we built the product right , with
7 of 37
respect to the informal requirements. But…
Informal Requirements
satisfies?
Implementation
translated
translated
checked/proved?
System Properties
Library of
Programming
Components uses
System Model
Using Formal Methods to Support the Certification Process
● DO-333 “Formal methods supplement to DO-178C and DO-278A” advocates the use of formal methods:
The use of formal methods is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analyses can contribute to establishing the correctness and robustness of a design.
● FMs, because of their mathematical basis, are capable of: ○ describing software system requirements.
Unambiguously
○ Enabling communication between engineers. ○ Providing verification evidence of:
● Aformalrepresentationofthesystembeinghealthy.
6 of 37 ● A formal representation of the system satisfying safety properties .
precise
Validation: Building the Right Product?
○ Successful checks/proofs ⇒ We built the right product. ○ The target of our checks/proofs may not be valid:
The requirements may be ambiguous, incomplete, or contradictory. ○ Solution: Precise Documentation
Chen-Wei Wang, Jonathan Ostroff, and Simon Hudon. Precise Documentation and Validation of Requirements. In FTSCS. Springer’s Communications in Computer and Information Science (CCIS), Volume 419, pp. 262 – 279, 2014.
Informal Requirements
satisfies?
Implementation
translated
translated
checked/proved?
System Properties
Library of
Programming
Components uses
System Model
8 of 37
Building the Right Product Right
Informal Requirements
validated
Precise Documentation of Requirements
satisfies?
Implementation
translated
translated
System Properties
checked/proved?
Library of Programming Components
certified
Certified Library of Programming
Components uses
System Model
● Use function tables to precisely document requirements ● Use the PVS theorem prover to:
9 of 37
○ library components
○ an implementation w.r.t. precise, validated requirements
Formulate
Verify
Darlington Shutdown Systems (SDSs)
● Two SDSs constitute a safety subsystem.
● Each SDS is a watchdog system that monitors system parameters of the in Ontario, Canada, and shuts down (i.e., trips) the reactor if it observes “bad” behaviour.
Darlington Nuclear Generating Station
● Both SDSs are physically isolated from the control system. ○ Fully isolated safety systems are much less complex than the
control systems.
○ This reduced problem complexity enables us to design, build,
and certify the behaviour of the safety system to a level of quality that would be difficult to achieve for an integrated (and thus more complex) system.
● Both SDSs are completely independent. 11 of 37
Cyber-Physical Systems (CPSs)
● Integrations of computation and physical processes
● With feedback loops, embedded computers monitor (via
sensors) and control (via actuators) the physical processes.
● The design of CPSs requires the understanding of the
joint dynamics of computers, software, networks, and physical
processes.
10 of 37
The Redesign Project of the Darlington SDSs
○ Ontario Hydro (now Ontario Power Generation Inc. – OPG) developed the original version of the SDS software in late 1980s.
○ When seeking for regulatory approval , the regulators were not convinced that the software would
● Performcorrectlyandreliably
● Remaincorrectandreliableundermaintenance
○ David Parnas suggested that a requirements/design document , using function tables, be constructed without referencing code.
● Averificationprocessconductedafterthedocumentvalidated. ● The regulators concluded that the software was safe for use .
A. Wassyng and M. Lawford. (2003) Lessons Learned from a Successful Implementation
of Formal Methods in an Industrial Project. FME.
12 of 37
Function Tables
● readable & precise documentation for complex relations
● suitable for documenting software requirements and design
● Two healthiness conditions:
○ completeness – no missing cases
○ disjointness – deterministic behaviour
[automated in PVS] [≥ one row is always true] [rows don’t overlap]
● used in Darlington nuclear reactor SDSs [e.g., f NOPsentrip] 13 of 37
NOP Example: Function Tables
Condition
∃i∈0..17 ● f NOPsentrip[i]=e Trip
Result
c NOPparmtrip
e Trip
e NotTrip
∀i ∈ 0 .. 17 ● f NOPsentrip[i] = e NotTrip Table: NOP Controller
Condition
Result
f NOPsentrip[i]
e Trip
(f NOPsentrip[i]) 1
−
e NotTrip
calibrated nop signal[i] ≥ f NOPsp
f NOPsp − k NOPhys < calibrated nop signal[i] < f NOPsp calibrated nop signal[i] ≤ f NOPsp − k NOPhys
Table: NOP sensor i, i ∈ 0 .. 17 (monitoring calibrated nop signal[i]) 15 of 37
Example: Neutron OverPower Unit of Darlington SDS
PLANT
calibrated_nop_signal[0] f_NOPsp ...
calibrated_nop_signal[17] f_NOPsp
c_NOPparmtrip
f_NOPsentrip[0]
... ...
f_NOPsentrip[17]
NOP SENSOR 0
NOP Controller
NOP SENSOR 17
○ NOP Controller depends on 18 instances of Sensor Trip units. ○ Each sensor i monitors two floating-point quantities:
● calibrated nop signal[i] [a calibrated NOP signal value]
● f NOPsp [set point value] ○ How do we formalize such informal requirements?
14 of 37
[ function tables! ]
Prototype Verification System (PVS)
● interactive environment
○ specifications using higher-order logic [predicates] ○ proofs using sequent-style deductions [inference rules]
● direct syntactic support of specifying tabular expressions ○ completeness & disjointness generated as proof obligations
● used for the Darlington SDSs
M. Lawford, P. Froebel, and G. Moum. (2004) Application of Tabular Methods to the Specification and Verification of a Nuclear Reactor Shutdown System. Formal Methods in System Design.
16 of 37
manufacturers refer to their programmable controller as a PLC, which stands for “programmable logic controller.”
Initially the PLC was used to replace relay logic, but its ever-increasing range of functions means that it is found in many
ture
empl of pe other comp
2
pet10882_ch01_0
are determined by the user program instead of the manner in which they are interconnected (Figure 1-4). Original equipment manufacturers can provide system updates by simply sending out a new program. End
Re-Implementation of the SDSs using PLCs
● Input-output behaviour of SDSs has been specified using function tables
● In the refurbishment project, we attempted to verify the re-implementation of SDSs using Programmable Logic Controllers (PLCs)
17 of 37
and more complex applications. Because the struc-
users can modify the program in the field, or if desired, security can be provided by hardware features such as
of a PLC is based on the same principles as those
oyed in computer architecture, it is capable not only
key locks and by software passwords.
• Lower Cost. PLCs were originally designe
place relay control logic, and the cost savin
been so significant that relay control is becoming
rforming relay switching tasks but also of performing
PLCs: Utilized in
applications such as timing, counting, calculating, aring, and the processing of analog signals.
Automating Industrial Process Control
(a) (a)
Programmable logic controller. Source: (a–b) Courtesy GE Intelligent Platforms.
Source: Photo courtesy Automation Direct, www.automationdirect.com. Source: Courtesy Rogers Machinery Company, Inc.
Figure 1-5 PLC communication module. Figure 1-26 PLC operator interface and monitor.
(b)
d to re- gs have
Chapter 1
01-016.indd 2
19 of 37
Figure 1-25
Programmable Logic Controllers (PLCs)
(b)
PLC installed in an industrial environment.
7/23/
Figure 1-1
Figure 1-6
High-speed counting.
Figure 1-27 Programmable automation controller (PAC). Source: Courtesy Banner Engineering Corp.
Source: (a–b) Courtesy Automation IG.
Software associated with a PLC but written and run on
Source: Photo courtesy Omron Industrial Automation, www.ia.omron.com. PLC Monitor
by blending the advantages of PLC-style control with
Electric, Ltd.
obsolete except for power applications. Generally, if an application has more than about a half-dozen
ibility; you ties and ty models, if be replaced
Modular
into which ture greatly ity. You ca manufactur modular co cessor mod operator int modules pl rack, it mak tacts called The PLC pr can commu
The pow that plug int this power field device
10
1.2 P
A typical P Figure 1-8. the input/o programmi PLC hardw both. An op connected manufactur ponents th with a clos etary, maki Most PLC sure that a is compati the princip gramming, ing, memo different m interchange
There ar
incorporate
(Figure 1-9
package wi
and I/O are
have a fixe
outputs. Th
lower cost.
usually can
9:00 PM
fixed I/O. O
Figu
A Visual Introduction to PLCs
Disclaimer: Many of the PLC and illustration diagrams below are originated from the book Programmable Logic Controllers (4th Edition; McGraw-Hill) by Frank D. Petruzella.
18 of 37
a personal computer falls into the following two broad that of PC-based systems. Such a device has been termed categories: a programmable automation controller, or PAC (Fig-
• PLC software that allows the user to program and
ure 1-27). Programmable automation controllers combi
document gives the user the tools to write a PLC
PLC ruggedness with PC functionality. Using PACs, y
PLCs: Replacing Relay-based Controllers
program—using ladder logic or another program-
can build advanced systems incorporating software cap
ming language—and document or explain the
bilities such as advanced control, communication, da logging,andsignalprocessingwithru(gag)edhardwareper- forming logic, motion, process control, and vision.
Figure 1-7 Control program can be displayed on a monitor 1.6 iPn rLeCal tSimiez.e and Application
ne ou a- ta
program in as much detail as is necessary.
• PLCsoftwarethatallowstheusertomonitor
and control the process is also called a human machine interface (HMI). It enables the user to view a process—or a graphical representation of a process—on a monitor, determine how the system is running, trend values, and receive alarm condi- tions (Figure 1-26). Many operator interfaces do not use PLC software. PLCs can be integrated with HMIs but the same software does not program both devices.
Most recently automation manufacturers have responded to the increased requirements of industrial control systems
12 Chapter 1 Programmable Logic Controllers (PLCs)
0882_ch01_001-016.indd 12
(a)
(a) Relay-based Control Panel
20 of 37
PLC
The criteria used in categorizing PLCs include functional-
easily trace and correct software and hardware prob-
ity, number of inputs and outputs, cost, and physical size
lems. To find and fix problems, users can display the
(Figure 1-28). Of these, the I/O count is the most impor-
control program on a monitor and watch it in real
tant factor. In general, the nano is the smallest size with
time as it executes (Figure 1-7).
less than 15 I/O points. This is followed by micro types
(15 to 128 I/O points), medium types (128 to 512 I/O
points), and large types (over 512 I/O points).
Figure 1-3 All the logic is contained in the PLC’s memory. Matching the PLC with the application is a key factor
4 Chapter 1 Programmable Logic Controllers (PLCs) in the selection process. In general it is not advisable to
Contactor
pet10882_ch01_001-016.indd 4
Light Solenoid
Outputs
(b)
(b) PLC-based Control Panel
Figure 1-2 Relay- and PLC-based control panels. (a) Rel based control panel. (b) PLC-based control panel.
Source: (a) Courtesy Mid-Illini Technical Group, Inc.; (b) Photo courtesy Ram
User program
7/23/10
9:01 PM
pet1
ay- co
•
Figu
are d
control relays, it will probably be less expensive to
u n
e
a
e
n s n b a
r o
e
t d
p a
n e
u u
e
s s
Electric, Ltd.
•
Program
Faster Response Time. PLCs are designed for high- Data
Example Issues
PLC
PLCs as Cyclic Executives:
years in many cases. Some processors have a capacitor
Pushbutton
Sensor
sometimes built into the processor module (Figure 2-44), can be used to copy a program from one PLC to another is provided by means of a separate pushbutton station. Manual pushbutton station
Inputs
Limit switch
derstanding for its users and has been modified to keep up
are determined by the user program.
• Faster Response Time. PLCs are designed for high- speed and real-time applications (Figure 1-6). The programmable controller operates in real time, which means that an event taking place in the
similar type PLC. Figure 1-17 Mixer process control problem. the last instruction that has been programmed, whsenrsoeraswsitches that close their respective contacts when
panels. (a) Relay- anel.
Photo courtesy Ramco
ns. Generally, ut a half-dozen ss expensive to
can communi-
er equipment to y control, data ocess parameters, s (Figure 1-5).
Figure 1-2
based control panel. (b) PLC-based control panel.
Source: (a) Courtesy Mid-Illini Technical Group, Inc.; (b) Photo courtesy Ramco
Figurfaeils1w-7hileCaonPtLroClpwriotghrflamashcamnebmeodriyspilsayreudnnoinga,mthoeniPtoLrC tFaicgtusrceal2le-4d5theHbaandc-khpeldanpreo,glroacmamteindgatetrtmhienarle.aroftherack. conditions reach their preset values.
field will result in the execution of an operation or output. Machines that process thousands of items per second and objects that spend only a fraction of a second in front of a sensor require the PLC’s quick-response capability.
The most popular method of PLC programming is to
control program on a monitor and watch it in redaevlices (pressurtehcsoiwsmitcphm,otweumneperircatsauurtepespwiltyciht,hdanodaepsPusLhn-oCt lanocnoatdriomntsoachlelrmyeep.sTluyappicpaellwypiruinpgsohcowbnnuecrtitotnosnfostrh,aes1e20-VAC
PLCs: Schematic
online and offline program editing, online program moni-
Using Theorem Proving toopeCrates rlikteitfrayditioCnalohamrdwipredocontreol npantesls.
• Easier to Troubleshoot. PLCs have resident diag- nostics and override functions that allow users to
4 Chapter 1 Programmable Logic Controllers (PLCs) toring, program documentation, diagnosing malfunctions
in the PLC, and troubleshooting the controlled system. Hard-copy reports generated in the software can be printed on the computer’s printer. Most software pack-
ages will not allow you to develop programs on another
manufacturer’s PLC. In some cases, a single manufac- turer will have multiple PLC families, each requiring its own software to program.
Human machine interfaces give the ability to the op- erator and to management to view the operation in real
7/27/10
User program
the
bat
ter
,
and
d
ata
handling for
Inputs, Outputs, Repeated Scans
Erasable Programmable Read-Only Memory
(EPROM) provides some level of security against unau-
thorized or unwanted changes in a program. EPROMs are
easily altered without special equipment. For example,
UV EPROMs (ultraviolet erasable programmable read-
only memory) can only be erased with an ultraviolet light.
EPROM memory is used to back up, store, or transfer PLC programs.
Electrically erasable programmable read-only mem-
different models. Consequently, PLC programs cannot be interchanged among different PLC manufacturers.
Figure 1-3 All the logic is contained in the PLC’s memory.
will resume running without having lost any working data
Contactor
Light
Outputs
Solenoid
designed so that data stored in them can be read, but not
incorporated into the PLC: fixed and modular. Fixed I/O
Programs in, e.g., ladder logic, are loaded into memory.
Programmable Logic Controllers (PLCs) Chapter 1 Input
module
3
7/23/10
Power supply module
pet10882_ch01_001-016.indd 4
9:58 PM
Input (b) sensing
Central
● Annex F of IEC 61131-3
Printers are used to provide hard-copy printouts of the
Relay- and PLC-based control panels. (a) Relay- devices
Processing M are determined by the user program.
Unit (CPU) Memory
Output load devices
● A formal approach to certifying the FB library ladder programs cannot be shown completely on a screen.
obsolete except for power applications. Generally,
install a PLC.
• CommunicationsCapability.APLCcancommuni-
speed and real-time applications (Figure 1-6). The programmable controller operates in real time, which means thatOapntiecvael nt taking place in the field will result inistohleateioxnecution of an operation or output. Machines that process thousands of items per second and objects that spend only a fraction of a second in front of a sensor require the PLC’s
time. A printout can show programs of any length and analyze the complete program.
if an application has more than about a half-dozen
Figure 2-48
control relays, it will probably be less expensive to
Optical
The PLC can have only one program in memory at a time. To change the program in the PLC, it is neces- sary either to enter a new program directly from the
isolation
Memory cartridge provides portable storage for user program.
cate with other controllers or computer equipment to
perform such functions as supervisory control, data Programming device
38 Chapter 2
24 of 37
PLC Hardware Components
gathering, monitoring devices and process parameters,
quick-response capability.
• Easier to Troubleshoot. PLCs have resident diag-
22 of 37
(a) Modular type
nostics and override functions that allow users to
and download and upload of programs (Figure 1-5).
Power supply
9:00 PM
Output module
Limit switch
● IEC 61131 Standard of PLCs 2.10 Recording and Retrieving Data
Processor
ModulePushbutton
Sensor
Figure 1-3
All the logic is contained in the PLC’s memory.
FiSgeuriarlepo1rt-6 High-speed counting.
is nonvolatile memory, it does not require battery backup.
Contactor
monitor inputs
Light
Solenoid
update outputs
cally, an EEPROM memory module is used to storew,itbhaPcLkCs. Its origin is based on electromechanical relay
Modular I/O (Figure 1-10) is divided by compartments
PLC
have a fixed number of connections built in for inputs and
execute program
sensor switch
Programmable Logic Controllers (PLCs) Chapter 1
3
Outputs
tion entering and editing, and navigation keys formmixeor mvo-tor is to be used to automatically stir the liquid
cessor module in which they reside. Flash memoryinsaavlastowhen thoeaptgeemerpaefrtaotureitanhdtepreufsasucererrefapochroprpgesreotagmram(Fmigiungrea2n-d4m8)o.nTithoerincga.rtTrihdege
User program
usually can be expanded by buying additional units of
(a)
Figure21-o4f3R7elationshipsbetweentheinputsandoutputs 23owfh3e7reitautomaticallybacksuppartsofRAM.IfTphoewproecressismraoncitkor,editwmithatekmepseratunreealnedcprtersiscuraelconnectionwithaseriesofcon-
Inputs
pet10882_ch01_001-016.indd
8
7/23/10
9:01 PM
Figure 1-4 Relationships between the inputs and outputs
Figure 2-42
Figure 1-5 PLC communication module.
manufacturers. Open architectures use off-the-shelf com- ponents that conform to approved standards. A system with a closed architecture is one whose design is propri- etary, making it more difficult to connect to other systems. Most PLC systems are in fact proprietary, so you must be sure that any generic hardware or software you may use is compatible with your particular PLC. Also, although the principal concepts are the same in all methods of pro-
PL
in
s
device.
PLC Monitor
be replaced.
Processor
after power is restored.
y is
disc
o
Battery used to back up processor RAM.
Processor Module
Flash Card
Source: Photo courtesy Automation Direct, www.automationdirect.com.
that provides at least 30 minutes of battery backup when Figure 2-44 Flash memory card installed in a socket on
C
a
gramming, there might be slight differences in address-
s
:
P
r
o
nne
g
cted
a
r
m
nd
pow
m
er is
O
Laptop computer
and I/O are packaged together, and the I/O terminals will
ory (EEPROM) is a nonvolatile memory that offers the same programming flexibility as does RAM. The EEPROM can be electrically overwritten with new data instead of
in Figure 2-45. This proprietary programming device has
being erased with ultraviolet light. Because the EEPROM
C
Source: Courtesy Banner Engineering Corp.
It provides permanent storage of the program and can be
Figure 2-46 Personal computer used as the programming changed easily using standard programming devices. Typi-
Source: Image Used with Permission of Rockwell Automation, Inc.
i
n
FlashEEPROMsaresimilartoEEPROMsinthabltoctkhse.RyLLwasoriginallydesignedforeasyuseandun-
andecaosymetsoinusthee.flTahsehsmeeumnoitrsy:ctohenytaairneemxutrletmifeulnycftaisotnatkseayvs-
and aingliaqnudidr-ectriyesvtianlg fidliessp.laInyad(LdiCtioDn), thoeryldioghnto-etmn1eiet.td3intogPrinciples of Operation
FF.
the processor.
g & De
Software
a
Hacnadn-hoenldy bperuosgerdafmormbearcskuaprsetorcaogme.pTahcet,maininexdpifefenrseinvcee,
with the increasintgyd.eYmaondus ocfainndusctrhy’os cosnterolfnreoedms. the modules available from the
ing around the program. Hand-held programmersvahlueasv. Ien addition, direct manual operation of the motor
limited display capabilities. Some units will display only
other units will display from two to four rungs of ladThdisecrontrol problem can be solved using the relay appropriate input module according to the manufacturer’s in real time. The PLC processor is also connected to the backplane and
n
cific manufacturer. Now let’s look at how a programmable logic controller also be used. This device would be hardwired to an appropri- lems. To find and fix problems, users can display the thAathpulumgaintmo tahcehrianceki(nFtiegrufraec1e-1(H1)M. FIo)rclarngebPeLcConsnysetcetmeds,to
logic. So-called intelligent hand-held programmers are
iring connections
method for moto
r dia -a
designed to support a certain family of PLCs from wahesnpbeot-h the pre
easily trace and correct software and hardware prob- The poPwLCerHasrudpwpalrye sCuopmploineesnDtsC Cphoawpter 2to other m3o7dules
manufacturer’s programming software (Figure 2-46).
lector switches, pilot lights, thumbwheels, and other op-
erator control panel devices (Figure 2-49). Luminescent
Typical capabilities of the programming software include
processor’s memory in ladder program format. Lengthy
●
Typically, a screen shows a maximum of five rungs at a Memory cartridge
pet10882_ch02_017-042.indd 38
7/23/10
9:06 PM
b
g,
me
mo
u
g
g
ry
a
i
n
g
I
lloc
atio
n
n
, re
tr
2.9 Programming Terminal Devices
t
e
package with no separate, removable units. The processor
A programming terminal device is needed to enter, mod-
ify, and troubleshoot the PLC program. PLC manufac-
turers use various types of programming devices. The
outputs. The main advantage of this typ
)
rdndrive) lower cost. The number of available I/O points varies and
simplest type is the hand-held type prog
w
be plugged into a PLC’s
irbatihlietyr ;thyaonuaahraenldi-mheitledddeinviwceh. at you can get in the quanti- ties and types dictated by the packaging. Also, for some
Figure 1-16 Typical PC software used to create a ladder logic program.
models, if any part in the unit fails, the whole unit has to
a connecting cable so that it can
A
fixed I/O. One disadvantage of fixed I/O is
i
programming port. Certain controllers use a plug-in panel
up, or transfer PLC programs (Figure 2-43). Figure 2-47 Copying programs to a computer har
resents rungs ofincotnotacwts, hcoiiclsh, ansdespeacriaal tinestrmuctoiodn ules can be plugged. This fea-
control. The relay ladder logic program graphically rep-
d
d
rive.
ture greatly increases your options and the unit’s flexibil-
m k a e n y u b f o a a c r t d u r e o r r a t n o d d m o i w x n t h l o e ma d a o n y n e w f a r y o
mdoridvuela(rFciognutrreol2le-r47co).nsSisotms oefCaPrUacsk,spuopwpoertsuthpepluy,seprof- a be physically removed from the processor for reproTgorgaetman-idea of how a PLC operates, consider the simple Temperature
diode (LED) window. There are usually keys for instruc-
process control pcreobslesmoirllumstroateduinleFig(uCreP1-U17.)H,eirenaput/output (I/O modules), and an ming; this can be done using the circuitry within the pro- memory cartridge that provides portable EEPROM stor-
modules plug into a rack. When a module is slid into the
2
r con
s
(
H
ss
rature switches are closed in Figure 1-19.
ure
and te
.
1
tr
ol s
M
1
hown in t
I
s
m
pe
)
H
a
n
he r
u
ela
m
y lad
a
c
h
i
de
M
g
gram of Figure 1c-1a8.nThce ommotormstaurtnericcoial (tMe) wis eintehrgizaeldl thfoer am12o0dVAuClemsodiunlartchoenfigruarecdkin.put module is shown
or when the manual pushbutton is pressed. The same output field device (motor starter coil) would
might be used for this application. The same input field ate output module according to the manufacturer’s addressing
use atipmeersaosniatlexceocmupteuste(Fr i(gPuCre) 1i-n7)c. onjunction with the field devices. With larger systems, power to field devices is
button) are used. These devices would be hardwired to an modular configured output module is shown in Figure 1-20.
pet10882_ch02_017-042.indd 37 8 Chapter 1 Programmable Logic Controllers (PLCs) 7/23/10 9:06 PM
iev
There are two ways in which I/Os (Inputs/Outputs) are
(Figure 1-9) is typical of small PLCs that come in one
dd
res
touch-screen keypads provide an operator interface that
r
al
sin
f
a
Pressure sensor
n
c
A
(D
i
e
e
o
ram
C
(In
C
ts
lack of flex-
sk
d
f
p
m
te
o
e
r
py
r
s
a
c
na
r
iv
outhdesciroem. Tphuetebrashiacrd ym
s
lo
wi
e
I
t
tch
catio
n
sc
he
e
m
r
f
e.
Ty
a
l
h
pi
k
h
e
c
e
cal
w
a
ging is
o
M
oto
r
IEC 61131-3 (ed 2.0, 2003): A Standard of PLCs
● Function Blocks (FBs): reusable components for programming PLCs.
● First published in 1993, IEC 61131-3 attempts to standardize the programming notations of PLCs using FBs:
○ IL (Instruction List)
○ ST (Structured Text)
○ LD (Ladder Diagram)
○ FBD (Function Block Diagram)
● There are three categories of FBs: ○ basic, stateless functions
[ e.g., +, ≥ 1, bcd2int ] [ e.g., hysteresis ] [e.g., limits alarm ]
○ basic FBs
○ composite FBs
25 of 37
Formal Verification of the FB Library: How?
IEC 61131-3 Standard
Natural Language Description
PVS Verification Environment
Correctness Correctness
Formalization
LEGEND
Manual translation
PVS verification
FB Requirements
Consistency
Consistency
FBD Specification
FBD Implementation
Formalization
Equivalence
ST Implementation
Formalization
1. Formalize FB requirements as function tables
2. Formalize ST and FBD implementations
3. Prove correctness and consistency of individual FBs
ST Specification
4. Identify issues in IEC 61131-3 Annex F & Propose solutions 27 of 37
Annex F of IEC 61131-3: A Function Block Library
● IEC 61131-3 Annex F lists a library of commonly-used FBs. ● PLC manufactures often provide a “IEC 61131-3 compliant”
FB library with their product.
● For the purpose of the re-implementation of SDS1 using FBs , we formally certify Annex F using:
[verification]
○ function tables [requirements specification]
○ PVS theorem prover
● Examined 29 FBs in the library, with a focus on implementations specified in ST and FBD:
○ 10 issues found [ambiguities, missing assumptions, errors] ○ Lack of precise, black-box requirements has led to these issues
unnoticed for ≥ 20 years! 26 of 37
Verification Results from Theorem Proving
Found issues in Annex F of IEC 61131-3:
1. Ambiguous behaviour
○ Incomplete timing diagrams: pulse timer ○ Implicit delay unit: sr block
2. Missing assumptions
○ input limits: ctud block, hysteresis alarm, limits alarm block
○ possible misusage: delay block
○ possible division-by-zero: average, pid ○ possible invalid array indexing: diffeq
3. Erroneous implementation
○ inconsistent implementations: stack int
For each issues, we propose a solution. 28 of 37
Example 1: Inconsistent Implementations for
STACK INT
○ The two alternative implementations are inconsistent as to when to push an item onto a LIFO stack:
29 of 37
FBD version specifies that the push operation is performed when the stack is already overflowed!
○ We proposed to add a negation gate between OFLO to EN. ○ Does it make sense to fix the ST implementation instead?
Example 2: Informal Requirements
31 of 37
Example 2: Up and Down Counters
○ An up-down counter (CTUD) consists of an up counter (CTU) and a down counter (CTD).
○ The output counter value CV is:
● (using the up counter) if a rising edge is detected on an input condition CU
Incremented
● ontheinputCD.(usingthedowncounter)ifarisingedgeisdetected
Decremented
Actions of increment and decrement are subject to a high limit PVmax
and a low limit PVmin.
○ The initial value of CV is:
● toapresetvaluePV ifaloadflagLDisTRUE
Loaded
● to 0 if a reset condition R is enabled
○ Two Boolean outputs are produced to reflect the change on CV :
Defaulted
● QU≡(CV>PV) 30of37 ● QD≡(CV<=0)
Example 2: Issues?
● What if ?
⇒ The of counter:
PVmin < CV < PVmax ≡ false
● What if LD ∧ PV ≤ PVmin (CV loaded with PV)?
In the next cycle, if CD is true, then the enabling condition of
:
false
PVmax < PVmin enabling condition
● What if 32 of 37
∧ ≥ ?
decrement
CD ∧ (CV > PVmin)
≡ {CVwaspresettoPV≤PVmin}
CD ∧ (PV > PVmin) ≡ { contriction }
LD PV PVmax
Example 2: Resolution?
Function Table!
Condition
CU∧¬CD ¬CU∧CD
Result
R
CV
0
LD
PV
CU ∧ CD
NC
CV−1< PVmax CV−1≥ PVmax CV−1> PVmin CV−1≤ PVmin
CV−1 +1 NC
¬R
¬LD
CV−1 -1 NC
NC
33 of 37
¬CU ∧ ¬CD
assume: PVmin < PV < PVmax
Index (1)
McMaster Centre for Software Certification
Acknowledgement of Collaborators
Developing Safety-Critical Systems
Professional Engineers: Code of Ethics
Using Formal Methods to
Support the Certification Process
Verification: Building the Product Right?
Validation: Building the Right Product?
Building the Right Product Right
Cyber-Physical Systems (CPSs)
Darlington Shutdown Systems (SDSs)
The Redesign Project of the Darlington SDSs
Function Tables
Example: Neutron OverPower Unit of Darlington SDS
35 of 37
Beyond this lecture . . .
Linna Pang, Chen-Wei Wang, Mark Lawford, and Alan Wassyng.
Formal Verification of Function Blocks Applied to IEC
61131-3. In Science of Computer Programming (SCP), Volume
113, December 2015, pp. 149 – 190.
34 of 37
Index (2)
NOP Example: Function Tables
Prototype Verification System (PVS)
Re-Implementation of the SDSs using PLCs
A Visual Introduction to PLCs
PLCs: Utilized in
Automating Industrial Process Control
PLCs: Replacing Relay-based Controllers
PLCs as Cyclic Executives:
Inputs, Outputs, Repeated Scans
PLCs: Schematic
PLCs: Programming & Debugging Interfaces
Using Theorem Proving to Certify Components
IEC 61131-3 (ed 2.0, 2003): A Standard of PLCs
Annex F of IEC 61131-3:
A Function Block Library
36 of 37
Index (3)
Verification Results from Theorem Proving
Example 1: Inconsistent Implementations for STACK INT
Example 2: Up and Down Counters
Example 2: Informal Requirements
Example 2: Issues?
Example 2: Resolution?
Beyond this lecture . . .
37 of 37
Formal Verification of the FB Library: How?