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

• Autorzy: Grobelna I. , Grobelny M.

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.

Słowa kluczowe

PL

diagramy aktywności UML; specyfikacja; model logiczny; weryfikacja modelowa; logika temporalna

EN

UML activity diagrams; specification; logical model; model checking; temporal logic

• Wydawca: Sieć Badawcza Łukasiewicz - Przemysłowy Instytut Automatyki i Pomiarów PIAP
• Czasopismo: Pomiary Automatyka Robotyka
• Rocznik: 2013
• Tom: R. 17, nr 10
• Strony: 188--192
• Opis fizyczny: Bibliogr. 16 poz., rys.

Twórcy

autor

Grobelna I.

• Instytut Informatyki i Elektroniki, Uniwersytet Zielonogórski

autor

Grobelny M.

• 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/].