Title :
Embedded Systems Modeling Language
Author :
Krystosik, Artur
Author_Institution :
Inst. of Comput. Sci., Warsaw Univ. of Technol.
Abstract :
Embedded System Modeling Language (EMLAN) is high-level, C-like 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. The paper presents the EMLAN language, methods of translation into DT-CSM and an example of specification and verification of the traffic light controller
Keywords :
concurrency control; embedded systems; formal specification; program verification; reachability analysis; simulation languages; C-like language; Embedded Systems Modeling Language; checking temporal formulas; data transformations; discrete time concurrent state machines; embedded systems software; hardware interactions; high-level language; model checking; reachability graph generation; synchronization mechanism; system partitioning; traffic light controller specification; traffic light controller verification; Automata; Binary decision diagrams; Computer science; Concurrent computing; Embedded software; Embedded system; Hardware; Lighting control; Medical control systems; Software systems;
Conference_Titel :
Dependability of Computer Systems, 2006. DepCos-RELCOMEX '06. International Conference on
Conference_Location :
Szklarska Poreba
Print_ISBN :
0-7695-2565-2
DOI :
10.1109/DEPCOS-RELCOMEX.2006.21
