Weryfikacja modelowa hierarchicznej specyfikacji sterownika logicznego

• Autorzy: Grobelna I. , Grobelny M.

Warianty tytułu

EN

Model checking of hierarchical logic controller specification

• Języki publikacji: PL

Abstrakty

PL

Specyfikacja zachowania projektowanego urządzenia powinna uwzględniać wszystkie elementy behawioralne. Z uwagi na złożoność projektowanych systemów szczególnie istotną rolę odgrywa możliwość dekompozycji. Z wykorzystaniem hierarchii można podzielić specyfikację na logiczne elementy połączone ze sobą na diagramach wyższego poziomu. W artykule przedstawiono zagadnienia związane z formalną weryfikacją hierarchicznych specyfikacji sterownika logicznego wyrażonych za pomocą interpretowanych sieci Petriego oraz diagramów aktywności języka UML.

EN

Specification of a designed logic controller should include all behavioral aspects. By complex systems design decomposition is especially valuable. Specification can be divided into parts using hierarchy. Logical elements are joined together at higher-level diagrams. The paper focuses on formal verification [1] of logic controller hierarchical specification by means of UML activity diagrams and interpreted Petri nets. Although hierarchy itself is presented in the considered specification techniques in different ways (complex activities by UML activity diagrams and macro-places/ macrotransitions by Petri nets), it is possible to use both techniques together in one project and to transform anytime one diagram into the another [5, 9, 10] (example in Figs. 1 and 2). In the transformation process, UML activity diagram actions correspond to Petri net transitions [7, 8]. Model checking [2, 3] of hierarchical specification can be performed step by step, e.g. by means of the NuSMV tool [11]. Rule-based specification (based on a Petri net) can be checked against behavioral properties [12, 13] expressed by temporal logic formulas [4]. Macroplaces can be verified separately (Fig. 3 considering local properties) and/or concurrently (Fig. 4, Fig. 5 considering mutual correlation and global properties). Next, the whole Petri net with macroplaces can be checked (Fig. 6). Sometimes it is convenient to verify a complete net (not hierarchical), like in [14]. Formal verification of specification can significantly increase its quality, and the support for hierarchy simplifies complex systems verification.

Słowa kluczowe

PL

hierarchia; interpretowane sieci Petriego; diagramy aktywności UML; weryfikacja modelowa

EN

hierarchy; interpreted Petri nets; UML activity diagrams; model checking

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2013
• Tom: R. 59, nr 8
• Strony: 796--798
• Opis fizyczny: Bibliogr. 14 poz., rys., wzory

Twórcy

autor

Grobelna I.

• Uniwersytet Zielonogórski, Podgórna 50, 65-246 Zielona Góra

autor

Grobelny M.

• Uniwersytet Zielonogórski, Podgórna 50, 65-246 Zielona Góra

Bibliografia

• [1] Kropf T.: Introduction to Formal Hardware Verification: Methods and Tools for Designing Correct Circuits and Systems. 1st edn, Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1999.
• [2] Emerson E. A.: The Beginning of Model Checking: A Personal Perspective. w O. Grumberg, H. Veith (ed.), 25 Years of Model Checking, Vol. 5000 of Lecture Notes in Computer Science, Berlin, Heidelberg: Springer-Verlag, s. 27-45, 2008.
• [3] Clarke E. M., Grumberg O., Peled D. A.: Model Checking. The MIT Press, 1999.
• [4] Ben-Ari M.: Logika matematyczna w informatyce. Klasyka informatyki, Wydawnictwa Naukowo-Techniczne, 2005.
• [5] Grobelny M., Grobelna I., Adamski M.: Hierarchical UML activity diagrams into control interpreted petri nets transformation. Mixed Design of Integrated Circuits and Systems - 19th international conference, Warszawa, Polska, s. 523-526, 2012.
• [6] Wrycza S., Marcinkowski B., Wyrzykowski K.: UML 2.0 w modelowaniu systemów informatycznych, Wydawnictwo Helion, 2005.
• [7] 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 – 17th International Conference, Wrocław, Polska, s. 607-612, 2010.
• [8] Grobelny M., Grobelna I.: Diagramy aktywności języka UML i sieci Petriego w systemach sterowania binarnego - od transformacji do weryfikacji. Pomiary, Automatyka, Kontrola, Vol. 56, nr 10, s. 1154-1158, 2010.
• [9] Grobelny M., Grobelna I., Adamski M.: Hardware behavioural modelling, verification and synthesis with UML 2.x activity diagrams. Proceedings of 11th IFAC/IEEE International Conference on Programmable Devices and Embedded Systems (PDeS), Brno, Czechy, s. 109-114, 2012.
• [10] Grobelny M., Grobelna I.: Diagramy aktywności UML w projektowaniu rekonfigurowalnych sterowników logicznych. Pomiary, Automatyka, Kontrola, Vol. 58, nr 7, s. 596-598, 2012.
• [11] Strona domowa narzędzia weryfikacji modelowej NuSMV: http:// nusmv.fbk.eu/
• [12] Grobelna I.: Weryfikacja modelowa specyfikacji sterowników logicznych. Oficyna Wydawnicza Uniwersytetu Zielonogórskiego, 2012.
• [13] Grobelna I.: Formal verification of embedded logic controller specification with computer deduction in temporal logic. Przegląd Elektrotechniczny, nr 12a, s. 40-43, 2011.
• [14] Grobelna I.: Control interpreted Petri Nets - model checking and synthesis. Petri Nets - manufacturing and computetr science, P. Pawlewski (ed.), InTech, s. 177-192, 2012.