Wprowadzenie do weryfikacji i symulacji w środowisku NuSMV

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

Abstrakty

PL

Specyfikacja systemu informatycznego jest jednym z pierwszych etapów jego tworzenia i stanowi fundament dalszych prac. Na tym etapie projektu określany jest sposób działania systemu oraz właściwości jego pracy. Należy zadbać o to, aby specyfikacja była w pełni poprawna, a zaprojektowany system spełniał wszystkie stawiane mu wymagania . Jedną z metod walidacji specyfikacji jest weryfikacja oraz symulacja modelu systemu. Oba zadania mogą zostać wykonane w środowisku NuSMV.

EN

The article is a short introduction into model checking and simulation in the NuSMV environment. The NuSMV tool allows description offinite state machines FSM and their verification using temporal logic formulas. Using a simple example (traffic lights), basic rules and commands of model checking and simulation process are presented. Using the NuSMV environment it is possible to detect some errors at an early stage of system development.

Słowa kluczowe

PL

specyfikacja systemu; sprawdzanie modelu; symulacja; NuSMV

EN

system speciflcation; model checking; simulation; NuSMV

• Czasopismo: Metody Informatyki Stosowanej
• Rocznik: 2011
• Tom: nr 1
• Strony: 23-30
• Opis fizyczny: Bibliogr. 13 poz., rys., tab.

Twórcy

autor

Grobelna, I.

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

Bibliografia

• [1] Ben-Ari M. Logika matematyczna w informatyce. Klasyka informatyki. Wydawnictwa Naukowo-Techniczne, Warszawa 2005
• [2] Cavada R. et al. NuSMV2.5 user manual, dostępne na http://nusmv.fbk.eu/
• [3] 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
• [4] Emerson E.A. The Beginning of Model Checking: A Personal Perspective, Lecture Notes in Computer Science, 25 Years of Model Checking: History, Achievements, Perspectives, 2008, str. 27 - 45
• [5] Fix L. Fifteen years of formal property verification in Intel, Lecture Notes in Computer Science (LNCS) 2008, Volume 5000/2008, Grumberg O., Veith H. (Eds.), str. 139 -144, 2008
• [6] 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
• [7] Grobelna I. Formalna weryfikacja maszyny stanów z wykorzystaniem logiki temporalnej, Pomiary, Automatyka, Kontrola, 2009, nr 7, str. 457 - 460
• [8] Grobelna I., Grobelny M. Gaps in design and tests of dependable embedded systems, Metody Informatyki Stosowanej, 2010, nr 2, str. 45-51
• [9] Grobelna I., Grobelny M., Adamski M. Petri Nets and activity diagrams in logic controller specification - transformation and verification, Mixed Design of Integrated Circuits and Systems - MKDES 2010, str. 607-612
• [10] Huth M., Ryan M. Logic in Computer Science. Modelling and Reasoning about Systems, Cambridge University Press 2004
• [11] 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, 1999, str. 123 - 193
• [12] Klimek R. Wprowadzenie do logiki temporalnej, AGH Uczelniane Wydawnictwa Naukowo-Dydaktyczne, Kraków 1999
• [13] Kropf T. Introduction to Formal Hardware Verification, ISBN 3-540-65445-3, Springer-Verlag Berlin Heidelberg New York, 1999