Asercyjne rozszerzenie języka ST normy IEC 61131-3 do dynamicznej weryfikacji systemów sterowania
Streszczenie
W pracy przedstawiono propozycję asercyjnego rozszerzenia języka ST (Structured Text) normy IEC 61131-3, nawiązującego do reguł projektowania kontraktowego i języka JML (Java Modeling Language). Zapisane asercje można przekształcić do kodu podczas kompilacji w celu uzyskania możliwości dynamicznej weryfikacji programów sterowania oraz detekcji błędów czujników. Przykłady dotyczą sterowania układem grzałek w zależności od temperatury oraz urządzenia do sortowania drewna.
Słowa kluczowe
język strukturalny ST, oprogramowanie, programowanie kontraktowe, system sterowania
Assertional extension in ST language of IEC 61131-3 standard for control systems dynamic verification
Abstract
The paper presents a proposition of assertional extension in Structured Text language from IEC 61131-3 standard, according to design by contract rules and JML (Java Modeling Language). Stored assertions could be converted to the code at compile time to obtain possibility of dynamic verification and for sensors failure detection. Heater control system and wood sorter machine are examples.
Keywords
control system, design by contract, software, Structured Text language
Bibliografia
- Baudin P., Cuoq P., Filliâtre J.Ch., Marché C., Monate B., Moy Y., Prevosto V.: ACSL: ANSI/ISO C Specification Language. http://frama-c.cea.fr.
- Bornat R.: Proving pointer programs in Hoare logic. Mathematics of Program Construction. MPC ‘00 Proceedings, pp. 102-126. Springer-Verlag, London, 2000.
- Filliâtre J.Ch. The WHY verification tool. Tutorial and Reference Manual. http://www.lri.fr.
- Kasprzyk J., Jegierski T., Wyrwał J., Hajda J.: Programowanie sterowników PLC. Wydawnictwo Pracowni Komputerowej Jacka Skalmierskiego, Gliwice, 1998.
- Leavens G.: An Overview of Larch/C++: Behavioral Specifications for C++ Modules. [w:] Kilov H., Harvey W. (red): Specification of Behavioral Semantics in Object-Oriented Information Modeling. Kluwer Academic Publishers, 1996.
- Leavens G., Baker A., Ruby C.: JML: a Notation for Detailed Design. [w:] Kilov H., Rumpe B., Simmonds I. (red): Behavioral Specifications of Businesses and Systems, 99.
- Meyer B.: Applying “design by contract”. Computer, 25(10), pp. 40-51, 1992.
- Meyer B.: Eiffel: The Language. Object-Oriented Series. Prentice Hall New York, 1992.
- Świder Z. (red.): Sterowniki mikroprocesorowe. Oficyna Wydawnicza Politechniki Rzeszowskiej, Rzeszów 2002.