Failure mode and effects analysis (FMEA) and model-checking of software for embedded systems by sequential scheduling of vectors of logic-labelled finite-state machines

Model-Driven Development (MDD) has proven to be a very powerful tool to produce software for embedded systems that control sophisticated equipment. It is therefore even more critical that such software be verified to be correct and to clearly understand what the safety implications of potential failures in sensors, actuators or faults of the software itself are. Using vectors of logic-labelled finite state machines, a clear semantics is obtained as well as executable models that provide the benefits that MDD promises. Since we can perform effective model-checking on these models, we show in this paper that we can use this to systematize and automate the failure mode and effect analysis of systems with embedded software. We illustrate this with two ubiquitous examples in the literature of model-checking for software in embedded systems.