View article

Many safety-concerned standards and regulations for real-time embedded systems, e.g., ISO 26262 for automotive electric/electronic systems, recommends the use of formal techniques to achieve the required safety level. This paper presents a method for formal analysis of real-time embedded systems. The method allows properties to be statistically checked early and quickly with high confidence, and may also produce a formal proof when required. This environment exploits uppaal tools consisting of a symbolic model checker (uppaal MC) and a statistical model checker (uppaal smc), and a model-based testing environment (uppaal Yggdrasil), all of which are based on a formal model in timed automata. We demonstrate our method on an industrial case, an automotive Turn Indicator System, showing how the design of the system at the early phase of system development may be efficiently checked …