Conversion of ST control programs to ANSI C for verification purposes

• Autorzy: Sadolewski J.
• Języki publikacji: EN

Abstrakty

EN

The paper presents a Behavioral Interface Specification Language for control programs written in ST language of IEC 61131-3 standard. The specification annotations are stored as special comments in ST code. The code and comments are then converted into ANSI C form for further transformation with Caduceus and Why tools. Verification of compliance between specification and code is performed in Coq.

Słowa kluczowe

EN

ST code; ANSI C; Behavioral Interface Specification Language; ST language

• Wydawca: Oficyna Wydawnicza Politechniki Wrocławskiej
• Czasopismo: e-Informatica Software Engineering Journal
• Rocznik: 2011
• Tom: Vol. 5, nr 1
• Strony: 65--76
• Opis fizyczny: Bibliogr. 12 poz.

Twórcy

autor

Sadolewski J.

• Department of Computer and Control Engineering, Rzeszow University of Technology,

Bibliografia

• [1] E. Tisserant, L. Bessard, and M. de Sousa, “An open source IEC 61131-3 integrated development environment,” in 5th Int. Conf. Industrial Informatics.Piscataway, NJ, USA, 2007.
• [2] B. Meyer, “Applying “design by contract”,”Computer, vol. 25, no. 10, p. 40–51, 1992.
• [3] J.-C. Filliâtre, T. Hubert, and C. Marché, “The Caduceus verification tool for C programs,” [online]http://caduceus.lri.fr, 2008.
• [4] J.-C. Filliâtre, “The Why verification tool.tutorial and reference manual,” [online]http://www.lri.fr, 2010.
• [5] Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development.Springer-Verlag, Berlin Heidelberg, 2004.
• [6] G. T. Leavens, A. L. Baker, and C. Ruby, JML:a Notation for Detailed Design, ser. Behavioral Specifications of Businesses and Systems, 1999.
• [7] E. W. Dijkstra, A Discipline of Programming.Prentice-Hall, Inc., 1976.
• [8] J. Sadolewski, Verification of complex programs for control systems, ser. Methods of producing and applying real time systems. Wydawnictwa Komunikacji i Łacznosci, 2010, (in Polish).
• [9] “Assertional extension in ST language of IEC 61131-3 standard for control systems dynamic verification,” Pomiary Automatyka Robotyka,no. 2, pp. 305–314, 2011, (in Polish).
• [10] R. Bornat, “Proving pointer programs in Hoare logic,” in Mathematics of Program Construction. Springer-Verlag. London, 2000, pp. 102–126.
• [11] D. Rzonca, J. Sadolewski, A. Stec, Z. Swider,B. Trybus, and L. Trybus, “Open environment for programming small controllers according to IEC 61131-3 standard,” Scalable Computing Practice and Experience, vol. 10, no. 3, pp.325–336, 2009.
• [12] K. D. Cooper and L. Torczon, Engineering a Compiler. Morgan Kaufmann, San Francisco,2003.