Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
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
Czasopismo
Rocznik
Tom
Strony
65--76
Opis fizyczny
Bibliogr. 12 poz.
Twórcy
autor
- Department of Computer and Control Engineering, Rzeszow University of Technology, js@prz-rzeszow.pl
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.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BPW7-0018-0061