Wprowadzenie do weryfikacji prostych programów w języku ST za pomocą narzędzi Coq, Why i Caduceus

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

Abstrakty

PL

Przedstawiono metodę przeprowadzania dowodów poprawności prostych programów sterowania napisanych w języku ST w środowisku Coq. Wykorzystano w tym celu dwa pomocnicze narzędzia Why i Caduceus należące do wspólnego projektu Proval. Metoda polega na ręcznej konwersji programu sterowania zapisanego w języku ST za pomocą przedstawionych reguł do równoważnej postaci w ANSI C. Ze względu na prostotę ST i podobieństwo do ANSI C nie powinno stanowić to problemu. Postać tę uzupełnia się o specyfikację wejść i wyjść a następnie poddaje automatycznym transformacjom programami Caduceus i Why. Program Why generuje lematy, które należy udowodnić, aby wykazać poprawność realizacji. Przedstawione reguły konwersji z języka ST do ANSI C stosuje się do przekształcania prostych bloków funkcjonalnych i programów. Zastosowanie niektórych reguł prowadzi do ograniczeń w liczbie instancji bloków, co jest wadą zaproponowanego rozwiązania. Wśród pozytywnych cech prezentowanych reguł wyróżnić można przejrzysty zapis specyfikacji i łatwość przeprowadzania dowodów w podobnych przypadkach.

EN

Based on three simple examples, the paper introduces into verification technique of control programs by means of Coq, Why and Caduceus tools developed in France. The examples involve binary multiplexer, RS fillip-flop and a Start-Stop circuit composed of theflip-flop and a gale. The programs to be verified are written in ST language (Structured Text) of lEC 61131-3 standard. The approach consists of four basic steps. First the original ST program is converted into ANSI C to be handled by Caduceus. This in turn converts the ANSI C into a code interpreted by Why. Coq is a proof assistant for verificaton of conditions generated by Why. Conversions and proofs for each of the examples are presented in details, together with trees involving tactics applied for verification. Based on these, some recommendations and hints how to handle problems of similar classes are given.

Słowa kluczowe

PL

coq; Why; Caduceus; asystent dowodzenia; transformacja kodu z języka ST do ANSI; kontrola programów i weryfikacja bloków funkcyjnych

EN

Coq; Why; Caduceus; proof assistant; ST to ANSI C conversion; control programs and function blocks verification

• Wydawca: Komisja Informatyki Polskiej Akademii Nauk, Oddział w Gdańsku
• Czasopismo: Metody Informatyki Stosowanej
• Rocznik: 2009
• Tom: nr 2 (19)
• Strony: 121--138
• Opis fizyczny: Bibliogr. 22 poz., rys., tab.

Twórcy

autor

Sadolewski J.

• Politechnika Rzeszowska, Wydział Elektrotechniki i Informatyki

Bibliografia

• [1] Affeldt R., Kobayashi N. Formalization and Verification of a Mail Server in Coq. Lecture Notes in Computer Science, v. 2609, Springer, 2003.
• [2] Bertot Y., Castéran P. Interactive Theorem Prooving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer-Verlag, 2004.
• [3] Bird R. Introduction to Functional Programming using Haskell. Prentice Hall, New York, 1998.
• [4] Bukowiec A., Węgrzyn M. Design of Logic Controllers for Safety Critical Systems Using FPGAs with Embeded Microprocessors. [w:] Colnaric M., Halang W. A., Węgrzyn M. (red.). Real-time programming 2004 (WRTP 2004): a proceedings volume from the 28th IFAC/IFIP Workshop, Oxford Elsevier Ltd, 2005.
• [5] Chailloux E., Manoury P., Pagano B. Developing Applications With Objective Caml. O'Reilly, Paris, 2000.
• [6] Dijkstra E. W. Umiejętność programowania. Wydawnictwa Naukowo Techniczne, Warszawa 1985.
• [7] Filliâtre J. Ch. The WHY verification tool. Tutorial and Reference Manual [online].http://www.lri.fr, [dostęp: 2009].
• [8] Filliâtre J. Ch., Hubert T., Marché C. The CADUCEUS verification tool for C programs [online]. http://caduceus.lri.fr, [dostęp: 2009].
• [9] Halang W., Śnieżek M. Bezpieczny sterownik logiczny. Oficyna Wydawnicza Politechniki Rzeszowskiej, Rzeszów, 1998.
• [10] Hooman J., Vain J. Integrating Methods for the Design of Real-Time Systems, Journal of Systems Architecture, v. 42, n. 6-7, 1996.
• [11] Howard W.A. The formulaes-as-types notion of construction. [w:] Hindley J. R. (red.).To H.B. Curry: Essays on Combinatory Logic, lambda-calculus and formalism. Seldin, 1980.
• [12] Huet G., Kahn G., Paulin-Mohring Ch. The Coq Proof Assistant. A Tutorial [online].http://coq.inria.fr/doc/main.html, [dostęp 2009].
• [13] IEC 61131–3 standard: Programmable Controllers-Part 3, Programming Languages.IEC, 2003.
• [14] Kerboeuf M., Novak D., Talpin J. P. Specification and Verification of a Steam-Boiler with Signal-Coq, University of Oxford, 2000.
• [15] Logika Formalna Zarys Encyklopedyczny. Marciszewski W. (red.). Państwowe Wydawnictwa Naukowe, Warszawa 1987.
• [16] Muzalewski M. An Outline of PC Mizar. Foundation Philippe le Hodey, Brussels, 1993.
• [17] Nipkow T., Paulson L. C., Wenzel M. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science v. 2283. Springer, 2002.
• [18] Owre S., Shankar N., Rushby J. M., Stringer-Calvert D. W. J. PVS System Guide. SRI International, 2001.
• [19] Parent C. Developing certified programs in the system Coq. The Program tactic. Research Report No 93-29, Lyon, 1993.
• [20] Storey N. Safety-Critical Computer Systems. Addison Wesley, 1996.
• [21] Strona domowa projektu Coq [online] http://coq.inria.fr, [dostęp: 2009].
• [22] The Coq Development Team. The Coq Proof Assistant Reference Manual, Ecole Polytechnique, INRIA, Universit de Paris-Sud, 2007.