PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

Weryfikowanie specyfikacji wymagań sterownika logicznego za pomocą diagramów aktywności UML, logiki temporalnej LTL i środowiska NuSMV

Treść / Zawartość
Identyfikatory
Warianty tytułu
EN
Verification of logic controller requirements specification by means of UML activity diagrams, LTL temporal logic and NuSMV tool
Języki publikacji
PL
Abstrakty
PL
W artykule przedstawiono ideę zastosowania diagramów aktywności UML do specyfikacji wymagań dotyczących zachowania sterownika logicznego. Lista wymagań podlegających weryfikacji zwykle definiowana jest bezpośrednio za pomocą formuł logiki temporalnej. Użycie przyjaznych dla użytkownika, powszechnie znanych i wykorzystywanych diagramów pozwala na prostsze i bardziej intuicyjne zapisanie wymagań. Diagramy są następnie formalnie przekształcane do formuł liniowej logiki temporalnej (LTL).
EN
The article introduces an idea to use UML activity diagrams [1-5] for specification of requirements regarding logic controller behavior. Requirements list to be verified [14] (using model checking technique [6, 7]) is usually directly defined using temporal logic formulas [12, 15]. Using user-friendly, commonly known and practiced diagrams allows to easier and more intuitively write down the requirements easier and more intuitively. Activity diagrams are then formally transformed into linear temporal logic (LTL) formulas. In this paper some sample UML activity diagrams which specify global properties are presented, together with their interpretation using LTL logic. To perform model checking process, model description (based i.e. on a control interpreted Petri net [8] or indirectly on an UML activity diagram [11]), and requirements list are needed. Afterwards it is checked, whether defined properties are satisfied in specified model description. If a requirement cannot be fulfilled, appropriate counterexample is generated allowing to localize error source. The article is structured as follows. Section 1 is an introduction. Background of a logic controller specification and its verification is presented in section 2. A novel approach to logic controller requirements definition using activity diagrams is shown in section 3. The paper ends with a short summary.
Rocznik
Strony
188--192
Opis fizyczny
Bibliogr. 16 poz., rys.
Twórcy
autor
  • Instytut Informatyki i Elektroniki, Uniwersytet Zielonogórski
autor
  • Katedra Mediów i Technologii Informacyjnych, Uniwersytet Zielonogórski
Bibliografia
  • 1. OMG Unified Modeling LanguageTM (OMG UML) Superstructure Version 2.4.1 - [www.omg.org/spec/UML/2.4.1/Superstructure/PDF]
  • 2. Graessle P., Baumann H., Baumann P., UML 2.x w akcji. Przewodnik oparty na projektach, Wydawnictwo Helion, 2006.
  • 3. Miles R., Hamilton K., UML 2.0. Wprowadzenie, Wydawnictwo Helion, 2007.
  • 4. Pender T., UML Bible, Wiley Publishing, Inc., 2003.
  • 5. Wrycza S., Marcinkowski B., Maślankowski J., UML 2.0 w modelowaniu systemów informatycznych, Wydawnictwo Helion, 2005.
  • 6. Clarke E.M., Grumberg O., Peled D.A., Model Checking, The MIT Press, 1999.
  • 7. Emerson E.A., The Beginning of Model Checking: A Personal Perspective [w:] Grumberg O., Veith H. (ed.), 25 Years of Model Checking, vol. 5000 of Lecture Notes in Computer Science, Berlin, Heidelberg: Springer-Verlag, 2008, 27-45.
  • 8. David R., Alla H., Discrete, Continuous, and Hybrid Petri Nets, 2nd ed., Springer Publishing Company, Incorporated, 2010.
  • 9. Grobelna I., Weryfikacja modelowa specyfikacji sterowników logicznych, Oficyna Wydawnicza Uniwersytetu Zielonogórskiego, Zielona Góra 2012.
  • 10. Grobelna I., Formal verification of embedded logic controller specification with computer deduction in temporal logic, „Przegląd Elektrotechniczny”, nr 12a, 2011, 40-43.
  • 11. Grobelny M., Grobelna I., Diagramy aktywności UML w projektowaniu rekonfigurowalnych sterowników logicznych, „Pomiary Automatyka Kontrola”, vol. 58, nr 7, 2012, 596-598.
  • 12. Ben-Ari M., Logika matematyczna w informatyce. Klasyka informatyki, Wydawnictwa Naukowo-Techniczne, 2005.
  • 13. Gomes L., Barros J., Costa A., Modeling Formalisms for Embedded System Design, Embedded Systems Handbook, Taylor and Francis Group, LLC, 2006.
  • 14. Kropf T., Introduction to Formal Hardware Verification: Methods and Tools for Designing Correct Circuits and Systems, 1st ed., Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1999.
  • 15. Huth M., Ryan M., Logic in Computer Science: Modelling and Reasoning about Systems, New York, USA: Cambridge University Press, 2004.
  • 16. NuSMV: a new symbolic model checker, NuSMV home page, [http://nusmv.fbk.eu/].
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-0c58c54f-ea55-4f08-862f-a5c3bae190df
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ć.