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

Formal Specification and Verification of Components for Industrial Logic Control Programming

Oscar Ljungkrantz (Institutionen för signaler och system, Automation) ; Knut Åkesson (Institutionen för signaler och system, Automation) ; Martin Fabian (Institutionen för signaler och system, Automation)
Proceedings of the 4th IEEE Conference on Automation Science and Engineering p. 935-940. (2008)
[Konferensbidrag, refereegranskat]

Component based approaches to develop industrial logic control programs promise to shorten development and modification times, and to lessen programming errors. However, to get these benefits it is important that components verified to work properly are reused. This work proposes using Reusable Automation Components (RACs), which contain not only the implementation but also a formal specification defining the correct use and behaviour of the component. This specification uses temporal logic to describe relations over time. The specification is helpful both for users of the components and for developers since the complete RAC including the specification can be translated into input to a tool for formal verification, to determine whether the specification is fulfilled or not. This paper shows how the RAC can be both implemented and specified using the common IEC 61131 standard and Ladder Diagrams. An industrial example is presented, specified and formally verified. It shows that RACs may help the developers to find errors and inconsistencies within the components, making it easier to do modifications of the code.



Denna post skapades 2008-12-01. Senast ändrad 2016-02-01.
CPL Pubid: 79236

 

Institutioner (Chalmers)

Institutionen för signaler och system, Automation

Ämnesområden

Information Technology

Chalmers infrastruktur