Portal de Periódicos da CAPES

Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools

2015; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-319-19458-5_4

1611-3349

Jin Hyun Kim, Kim G. Larsen, Brian Nielsen, Marius Mikučionis, Petur Olsen,

Software Testing and Debugging Techniques

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 against the defined system requirements.