PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

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

Identyfikatory
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.
Twórcy
autor
autor
  • 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.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BPG5-0029-0036
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.