Nowa wersja platformy jest już dostępna.
Przejdź na https://bibliotekanauki.pl

PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2008 | nr 3 (Tom 16) | 107--124
Tytuł artykułu

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

Autorzy
Warianty tytułu
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.
Wydawca

Rocznik
Strony
107--124
Opis fizyczny
Bibliogr. 20 poz., rys., tab.
Twórcy
autor
  • 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
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.baztech-d6e5acf9-01e3-4867-96f9-801e8790e757
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.