This Article 
 Bibliographic References 
 Add to: 
Safety Assurance in Process Control
January/February 1994 (vol. 11 no. 1)
pp. 61-67

Programmable logic controllers are popular in process-control applications, but the software can be very complex. To make it easier to verify the safety of PLC software, we have created a rigorous process that uses formal specifications of function blocks, which are typically used in safety-critical control and automation applications. Key to the process is the use of Obj, an algebraic language that lets you specify requirements and designs independently of any data representation and implementation. We also used the Obj3 system, which supports the latest version of Obj with an interpreter and a functional programming environment, to automate parts of the specification testing and formal verification.

Index Terms:
safety; software reliability; programmable controllers; process computer control; formal specification; functional programming; formal verification; safety assurance; process control; programmable logic controllers; PLC software safety; formal specifications; function blocks; safety-critical control; Obj; algebraic language; requirements specification; design specification; data representation; Obj3 system; interpreter; functional programming environment; specification testing; formal verification
Wolfgang A. Halang, Bernd J. Krämer, "Safety Assurance in Process Control," IEEE Software, vol. 11, no. 1, pp. 61-67, Jan.-Feb. 1994, doi:10.1109/52.251211
Usage of this product signifies your acceptance of the Terms of Use.