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

Type: Article

Number of downloads: 1946

Download resource

PDF

Cite

BibTeX EndNote

Title: EMLAN: język modelowania i formalnej weryfikacji oprogramowania systemów wbudowanych
Variant of the title: EMLAN: Language for modeling and formal verification of embedded systems
Author: Krystosik, Artur
Published in: Czasopismo Techniczne. Informatyka
Numbering: R. 105, Z. 24, 1-I
Release date: 2008
Place of publication: Kraków
Publisher: Wydawnictwo PK
Language: Polish
Abstract: 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.
PKT classification: 410000 Informatyka
Department: Zbiory cyfrowe BPK
License: Licencja PK. Brak możliwości edycji i druku.
Access rights: Zasób dostępny dla wszystkich