UML Verification with Verics

• Autorzy: Niewiadomski A. , Penczek W.
• Języki publikacji: EN

Abstrakty

EN

We show how to verify UML specifications against properties expressed by CTL-like formulas using the symbolic model checker Verics. Our method is illustrated with an example showing a verification of Alternating Bit Protocol.

Słowa kluczowe

EN

model checking; UML; unified modeling language; VerICS

• Wydawca: Wydawnictwo Uniwersytetu Przyrodniczo-Humanistycznego w Siedlcach
• Czasopismo: Studia Informatica : systems and information technology
• Rocznik: 2007
• Tom: Vol. 1(8)
• Strony: 19--31
• Opis fizyczny: Bibliogr. 12 poz., rys., tab.

Twórcy

autor

Niewiadomski A.

• Institute of Computer Science, University of Podlasie, ul. Sienkiewicza 51, 08-110 Siedlce, Poland

autor

Penczek W.

• Institute of Computer Science, University of Podlasie, ul. Sienkiewicza 51, 08-110 Siedlce, Poland
• Institute of Computer Science, Polish Academy of Science, ul. Ordona 21, 01-237 Warsaw, Poland

Bibliografia

• 1. OMG: Unified Modeling Language (UML), version 2.0. http://www.omg.org/technology/documents/formal/uml.htm (2005).
• 2. Nabiałek, W., Niewiadomski, A., Penczek, W., Półrola, A., Szreter, M.: VerlCS 2004: A model checker for real time and multi-agent systems. In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’04). Volume 170(1) of Informatik-Berichte., Humboldt University (2004) 88-99.
• 3. Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerlCS: A tool for verifying timed automata and Estelle specifications. In: Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03). Volume 2619 of LNCS., Springer-Verlag (2003) 278-283.
• 4. Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: The IF toolset. In Bernardo, M., Corradini, F., eds.: SFM. Volume 3185 of Lecture Notes in Computer Science., Springer (2004) 237-267.
• 5. Knapp, A., Merz, S., Rauh, C.: Model checking - timed UML state machines and collaborations. In: FTRTFT. (2002) 395-416.
• 6. Sharygina, N., Browne, J., Xie, F., Kurshan, R., Levin, V.: Lessons learned from model checking a NASA robot controller. Formal Methods in System Design 25 (2004) 241-270.
• 7. Starr, L.: Executable UML: The models that are the code. In: Model Integration, LLC. (2001).
• 8. Apvrille, L., Courtiat, J.P., Lohr, C., de Saqui-Sannes, P.: TURTLE: A real-time UML profile supported by a formal validation toolkit. In: IEEE Trans. Software Eng 30(7) (2004) 473-487.
• 9. Doroś, A., Janowska, A., Janowski, P.: From specification languages to timed automata. In: Proc. of CS&P the Int. Workshop on Concurrency, Specification and Programming (CS&P’02). Volume 161(1) of Informatik-Berichte., Humboldt University (2002) 117-128.
• 10. Penczek, W., Woźna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae 51(1-2) (2002) 135-156.
• 11. Woźna, B., Penczek, W., Zbrzezny, A.: Reachability for timed systems based on SAT-solvers. In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’02). Volume 161(2) of Informatik-Berichte., Humboldt University (2002) 380-395.
• 12. Zhang, L.: zChaff http://www.ee.princeton.edu/~chaff/zchaff.php (2005).