| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 5003174 | IFAC Proceedings Volumes | 2006 | 6 Pages |
Abstract
Embedded System Modelling Language (EMLAN) is high-level, C-like language for modelling and model checking of embedded systems. The language addresses a number of topics concerning embedded systems 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 and checking requirements expressed as CTL temporal formulas. The paper presents the EMLAN language, methods of translation into DT-CSM and an example of specification and symbolic verification of the traffic light controller.
Related Topics
Physical Sciences and Engineering
Engineering
Computational Mechanics
Authors
Artur Krystosik, Dariusz Turlej,