Emlan: A Language for model checking of embedded systems software

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.