Formalna analiza interpretowanych algorytmicznych maszyn stanów ASM z wykorzystaniem narzędzia model checker

• Autorzy: Grobelna I.
• Języki publikacji: PL

Abstrakty

EN

Algorithmic state machines ASM are one of formal methods of embedded systems specification. They are defined during system project phase. Potential not detected errors in specification may generate unnecessary costs, and in case of dependable systems they may even have catastrophic causes. The article presents formal verification and analysis method of algorithmic state machines using computer deduction in temporal logic (Model Checking technique). Model checker tools enable automatic verification of system specification by checking consistency between model description and requirements which have to be satisfied in the model. The paper concentrates on NuSMV model checker. Formal verification technique Model Checking is discussed basing on presented case study.

Słowa kluczowe

EN

algorithmic state machines; temporal logic; formal verification; Model Checking

• Wydawca: Komisja Informatyki Polskiej Akademii Nauk, Oddział w Gdańsku
• Czasopismo: Metody Informatyki Stosowanej
• Rocznik: 2008
• Tom: nr 3 (Tom 16)
• Strony: 107--124
• Opis fizyczny: Bibliogr. 20 poz., rys., tab.

Twórcy

autor

Grobelna I.

• Uniwersytet Zielonogórski, Wydział Elektrotechniki, Informatyki i Telekomunikacji

Bibliografia

• [1] Klimek R. Wprowadzenie do logiki temporalnej. AGH Uczelniane Wydawnictwa Naukowo-Dydaktyczne, Kraków 1999
• [2] Huth M., Ryan M. Logic in Computer Science. Modelling and Reasoning about Systems. Cambridge University Press 2004
• [3] Eshuis R. Symbolic Model Checking of UML Activity Diagrams. ACM Transactions on Software Engineering and Methodology, Vol. 15, No. 1, styczeń 2006, str. 1-38
• [4] Cavada R. et al. NuSMV 2.4 User Manual
• [5] Clarke E.M., Wing J. M. et al. Formal methods: State of the Art and Future Directions. ACM Computing Surveys, Vol. 28, No. 4, grudzień 1996
• [6] Andrzejewski G. Programowy model interpretowanej sieci Petriego dla potrzeb projektowania mikrosystemów cyfrowych. Oficyna Wydawnicza Uniwersytetu Zielonogórskiego 2003, str. 16-26
• [7] Fisler K. A logical formalization of hardware design diagrams. Indiana University Technical Report 416, wrzesień 1994
• [8] Arnold M. G., Cowles J. R., Joslin R. D., Cupal J. J. Simulation of cooperating algorithmic state machines using Verilog HDL. International Conference on Simulation and Hardware Description Languages (ICSHDL), 24-26 stycznia 1994, Tempe, Arizona, (edytorzy P.A. Widsey oraz D. Rhodes), The Society for Computer Simulation, str. 63-69
• [9] Davis J.P., Wake H.A., Leehaug C., Branton J., Namilae N. Design versus Programming in Custom Computing Machine Applications: Experiences Using the Algorithmic State Machine Method. Proceedings Military Applications of Programmable Logic Devices – MAPLD-2004, Washington, DC, 8-10 września 2004
• [10] Adamski M., Chodań M. Modelowanie układów sterowania dyskretnego z wykorzystaniem sieci SFC. Wydawnictwo Politechniki Zielonogórskiej, Zielona Góra 2000
• [11] David R., Alla H. Petri Nets & Grafcet. Tools for modeling discrete event systems. Prentice Hall 1992
• [12] Grobelna I. Formal verification of logic controller specification using NuSMV model checker. X Międzynarodowe Warsztaty Doktoranckie OWD’2008, Archiwum konferencji PTETIS, Vol. 25, październik 2008, str. 459-464
• [13] Girish K.P. An introduction to model checking. February 2004, http://www.embedded.com
• [14] Ribeiro Ó.R., Fernandes J.M., Pinto L.F. Model Checking Embedded Systems with PROMELA. Proceedings of the 12th IEEE International Conference and Workshops on Engineering of Computer-Based Systems (ECBS’05), 2005, str. 378-385
• [15] Ben-Ari M. Logika matematyczna w informatyce. Klasyka informatyki. Wydawnictwa Naukowo-Techniczne, Warszawa 2005
• [16] Adamski M. A rigorous design methodology for reprogrammable logic controllers. The International Workshop on Discrete-Event System Design, DESDes’01, czerwiec 2001, Przytok
• [17] Gomes L., Barros J.P., Costa A. Modeling Formalisms for Embedded System Design. Embedded Systems Handbook, Taylor & Francis Group, LLC, 2006
• [18] Kern C., Greenstreet M.R. Formal Verification in Hardware Design: A Survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), Vol. 4, Issue 2, kwiecień 1999, str. 123-193
• [19] Stroud C.E. An Overview of BIST, Frontiers in Electronic Testing, Vol. 19, A Designer’s Guide to Built-In Self-Test, Springer US 2002, str. 1-14
• [20] Adamski M. Projektowanie układów cyfrowych systematyczną metodą strukturalną, Wydawnictwo Wyższej Szkoły Inżynierskiej w Zielonej Górze, Zielona Góra 1990