Issue No. 01 - January/February (1994 vol. 11)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/52.251211
<p>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.</p>
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
B. J. Krämer and W. A. Halang, "Safety Assurance in Process Control," in IEEE Software, vol. 11, no. , pp. 61-67, 1994.