EMLAN: język modelowania i formalnej weryfikacji oprogramowania systemów wbudowanych

• Autorzy: Krystosik, A. , Gawkowski, P.

Warianty tytułu

EN

EMLAN: a language for modeling and formal verification of embedded systems software

• Języki publikacji: PL

Abstrakty

PL

Embedded System Modeling Language (EMLAN) jest wysokiego poziomu językiem modelowania i formalnej weryfikacji oprogramowania systemów wbudowanych. Mechanizmy języka pozwalają na modelowanie rozmaitych aspektów systemu wbudowanego, takich jak: współbieżność, przerwania, mechanizmy synchronizacji, czas, operacje na danych, interakcja oprogramowania ze sprzętem. Formalna weryfikacja specyfikacji EMLAN oparta jest o metody weryfikacji modelowej. Polega na translacji modelu systemu wyrażonego w języku EMLAN do systemu automatów DT-CSM (Discrete Time Concurrent State Machines), generacji grafu stanów osiągalnych i badaniu jego własności temporalnych przy wykorzystaniu logiki CTL. Przykładem zastosowania jest weryfikacja oprogramowania systemu alarmu samochodowego.

EN

Embedded System Modeling Language (EMLAN) is high-level, C-like language for modeling and model check-ing the embedded systems software. The language addresses a number of topics such as: partitioning of the sys-tem, concurrency, interrupts, synchronization mechanisms, time, data transformations, hardware interactions. Model checking of the EMLAN specification is based on translations into DT-CSM (Discrete Time Concurrent State Machines), generation of a reachability graph (represented in BDD) and checking temporal formulas (CTL) representing requirements. The paper presents the EMLAN language, methods of translation into DT-CSM and an example of specification and verification of car immobilizer.

Słowa kluczowe

PL

język EMLAN; automat DT-CSM; oprogramowanie systemów wbudowanych; weryfikacja autoalarmu samochodowego

EN

EMLAN language; embedded systems software; DT-CSM; verification of car immobilizer

• Czasopismo: Zeszyty Naukowe Wydziału ETI Politechniki Gdańskiej. Technologie Informacyjne
• Rocznik: 2007
• Tom: T. 13
• Strony: 331-338
• Opis fizyczny: Bibliogr. 7 poz., rys., tab.

Twórcy

autor

Krystosik, A.

autor

Gawkowski, P.

• Wydział Elektroniki i Technik Informacyjnych, Instytut Informatyki, Politechnika Warszawska

Bibliografia

• [1] Bryant R. E. (1995). Binary Decision Diagrams: Enabling Technologies for Formal Verification. Proc. IEEE/ACM Int. Conf. on Computer-Aided Design, pp. 236-243, 1995.
• [2] Daszczuk W. B. (2003). Verification of temporal properties in concurrent systems. Ph.D. thesis, ICS WUT 2003.
• [3] Halbwachs N., Peled D. (1999). NuSMV: a new symbolic model verifier. Proceeding of International Conference on Computer-Aided Verification (CAV'99). In Lecture Notes in Computer Science, number 1633, pages 495-499, Trento, Italy, July 1999. Springer.
• [4] Holzmann G.J. (1997). The Model Checker Spin. IEEE Transactions On Software Engineering, Vol. 23, No. 5, May 1997.
• [5] Mieścicki J. (1992b). Concurrent system of communicating machines. Institute of Computer Science, WUT, Research Report 35/92.
• [6] J. Sosnowski, P. Gawkowski, Embedded System dependability evaluation with simulation tools, Proc. of IFAC Workshop on Programmable Devices and Embedded Systems, 2006, str. 180-185.
• [7] Wilczyński, J. Sosnowski, P. Gawkowski, Flexible microcontroller Simulator for testing purposes, Proc. of IFAC Workshop on Programmable Devices and Embedded Systems, 2004, str. 310-315.