Specification and verification of simple logic control programs using Frama C

• Autorzy: Sadolewski J. , Świder Z.

Warianty tytułu

PL

Specyfikacja i weryfikacja prostych programów sterowania logicznego z wykorzystaniem Frama C

• Języki publikacji: EN

Abstrakty

EN

The paper presents an approach to verification process for programs of simple logic controls written in ANSI C. The software is verified with open source tools like Frama C, Jessie and Coq. Process of specification determination and verification whether implementation conforms with specification is demonstrated by several examples, involving combinatorial logic, sequential logic and sequential logic with time constraints.

PL

W artykule zaproponowano proces weryfikacji prostych programów sterowania logicznego napisanych w ANSI C. Programy są weryfikowane przez ogólnodostępne narzędzia, jak Frama C, Jessie i Coq. Proces określania specyfikacji i weryfikacji zgodności specyfikacji z implementacją przedstawiono na kilku przykładach układów kombinacyjnych, sekwencyjnych oraz sekwencyjnych z uzależnieniami czasowymi.

Słowa kluczowe

EN

software verification; control system; Frama C

PL

weryfikacja programów; system sterowania; Frama C

• Wydawca: Wydawnictwo Politechniki Śląskiej
• Czasopismo: Studia Informatica
• Rocznik: 2011
• Tom: Vol. 32, nr 3B
• Strony: 21--34
• Opis fizyczny: Bibliogr. 10 poz.

Twórcy

autor

Sadolewski J.

autor

Świder Z.

• Rzeszów University of Technology, Department of Computer and Control Engineering, ul. W. Pola 2, 35-959 Rzeszów, Poland,

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. Baudin P., Cuoq P., Filliâtre J.Ch., Marché C., Monate B., Moy Y., Prevosto V.: ACSL: ANSI/ISO C Specification Language. INRIA, 2009.
• 3. Coq homepage [online] http://coq.inria.fr.
• 4. Dijkstra E.W.: A Discipline of Programming. Prentice-Hall Inc., Englewood Cliffs, NJ 1976.
• 5. Frama C homepage [online] http://frama-c.ceq.fr.
• 6. Kalisz J.: Podstawy elektroniki cyfrowej. WKŁ, Warszawa 2007.
• 7. Kerbœuf M., Novak D., Talpin J. P.: Specification and Verification of a Steam-Boiler with Signal-Coq, University of Oxford, 2000.
• 8. Świder Z. (red ): Sterowniki mikroprocesorowe. Oficyna Wydawnicza Politeclmiki Rzeszowskiej, 2002.
• 9. Moy Y., Marché C.: Jessie Plugin Tutorial, [online] http://why.lri.fr.
• 10. Sadolewski J.: Introduction to verification simple programs in ST language with Coq, Why and Caduceus. Metody Informatyki Stosowanej. No. 2(19) 2009 (in Polish).