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

Typ: Artykuł

Liczba pobrań: 1829

Pobierz zasób

PDF

Cytuj

BibTeX EndNote

Tytuł: EMLAN: język modelowania i formalnej weryfikacji oprogramowania systemów wbudowanych
Wariant tytułu: EMLAN: Language for modeling and formal verification of embedded systems
Autor: Krystosik, Artur
Opublikowane w: Czasopismo Techniczne. Informatyka
Numeracja: R. 105, Z. 24, 1-I
Data wydania: 2008
Miejsce wydania: Kraków
Wydawca: Wydawnictwo PK
Język: polski
Abstrakt: 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.

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.
Klasyfikacja PKT: 410000 Informatyka
Wydział: Zbiory cyfrowe BPK
Licencja: Licencja PK. Brak możliwości edycji i druku.
Prawa dostępu: Zasób dostępny dla wszystkich