Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools
verfasst von : Jin Hyun Kim, Kim G. Larsen, Brian Nielsen, Marius Mikučionis, Petur Olsen
Erschienen in: Formal Methods for Industrial Critical Systems
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.