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.