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

• Autorzy: Krystosik A.

Warianty tytułu

EN

EMLAN: Language for modeling and formal verification of embedded systems

• 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. Formalna weryfikacja 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 systemu i badaniu jego własności temporalnych z wykorzystaniem logiki CTL. Przykładem zastosowania jest weryfikacja oprogramowania systemu alarmu samochodowego.

EN

Embedded System Modeling Language (EMLAN) is high-level language for modeling and model checking the embedded systems software. The language addresses a number of topics such as: partitioning of the system, 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. As an example a verification of car alarm system is given.

Słowa kluczowe

PL

formalna weryfikacja; modelowanie; systemy wbudowane

EN

embedded system; formal verification; modelling

• Wydawca: Wydawnictwo Politechniki Krakowskiej im. Tadeusza Kościuszki
• Czasopismo: Czasopismo Techniczne. Informatyka
• Rocznik: 2008
• Tom: R. 105, z. 1-I
• Strony: 33--44
• Opis fizyczny: Bibliogr. 9 poz.,Rys., tab.,

Twórcy

autor

Krystosik A.

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

Bibliografia

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