Wyniki wyszukiwania - Biblioteka Nauki

Ten serwis zostanie wyłączony 2025-02-11.

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

1 Zeszyty Naukowe Wydziału ETI Politechniki Gdańskiej. Technologie Informacyjne

1 2007

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: DT-CSM

Sortuj według:

Ogranicz wyniki do:

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

100%

Krystosik A. , Gawkowski P.

Zeszyty Naukowe Wydziału ETI Politechniki Gdańskiej. Technologie Informacyjne

2007

tom T. 13

331-338

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.

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.