Article Preview
TopIn (Bourahla, 2009), author has presented an approach for the analysis of real-time embedded systems. The analysis is based on the verification of the schedulability of tasks in addition to the verification of requirements on the overall system. In (Sammi, 2010), authors have presented a survey about the formal specification languages which are used to specify Real-time systems, then they have compared formal languages which are used to specify real-time systems such as VDM++, RTSJ, ASTRAL. A comparison criterion was established to select the best suitable specification languages for Real-Time systems.
In (Boucherit, 2011), authors have proposed a new formal approach based on rewriting logic, in which they attempted to bridge the gap between agent based system analysis and its specification. In addition, their approach included a well-known and effective verification technique, model checking, and allowed independent of the used formalism to verify an important number of properties deemed relevant on critical system based on agent paradigm.
In (Basit, 2014a), a methodology has been proposed for the modeling and verification of embedded systems in parallel and distributed environments. Authors have demonstrated the suitability of the framework by applying it on the case study of embedded security system. The case study was modeled using SysML's state machine diagrams and then semantics were described to translate these state machine diagrams to DVE (DiVinE) based model. The translated model is verified against specified LTL properties using DiVinE.