CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Towards Industrial Formal Specification of Programmable Safety Systems

Oscar Ljungkrantz (Institutionen för signaler och system, Automation) ; Knut Åkesson (Institutionen för signaler och system, Automation) ; Chengyin Yuan ; Martin Fabian (Institutionen för signaler och system, Automation)
IEEE TRANSACTIONS ON CONTROL SYSTEMS TECHNOLOGY (1063-6536). Vol. 20 (2012), 6, p. 1567-1574.
[Artikel, refereegranskad vetenskaplig]

Formal methods for specification and verification are promising in developing PLC (Programmable Logic Controller) programs in manufacturing industry. Particularly this holds for safety PLCs, used to protect humans and equipment from injuries and damages. An important challenge though, is the development of formal specifications, typically a tough task for control engineers. This paper proposes a systematic work procedure that can be used as a first step of developing formal specifications of safety PLC programs in industry. The work procedure intends to facilitate the development of relevant formal properties for safety PLC program components. The formal specifications can be used for automatic formal verification of the components, using model checking techniques. The paper shows how the work procedure has been applied to industrial safety components, resulting in relevant and nontrivial specifications.

Nyckelord: manufacturing automation software, programmable logic controller (PLC), safety logic, software requirements and specifications, formal specification

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2011-09-13. Senast ändrad 2016-02-01.
CPL Pubid: 146128


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för signaler och system, Automation (2005-2017)


Information Technology

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:

On Formal Specification and Verification of Function Block Applications in Industrial Control Logic Development