Tytuł artykułu
Autorzy
Identyfikatory
Warianty tytułu
Specyfikacja i weryfikacja prostych programów sterowania logicznego z wykorzystaniem Frama C
Języki publikacji
Abstrakty
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.
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.
Czasopismo
Rocznik
Tom
Strony
21--34
Opis fizyczny
Bibliogr. 10 poz.
Twórcy
autor
autor
- Rzeszów University of Technology, Department of Computer and Control Engineering, ul. W. Pola 2, 35-959 Rzeszów, Poland, js@prz-rzeszow.pl
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).
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BSL2-0025-0080