Embedded Systems Modeling Language

Author

Krystosik, Artur

Author_Institution

Inst. of Comput. Sci., Warsaw Univ. of Technol.

fYear

2006

fDate

25-27 May 2006

Firstpage

27

Lastpage

34

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Dependability of Computer Systems, 2006. DepCos-RELCOMEX '06. International Conference on

Conference_Location

Szklarska Poreba

Print_ISBN

0-7695-2565-2

Type

conf

DOI

10.1109/DEPCOS-RELCOMEX.2006.21

Filename

4024029