Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
2016 (English)In: FM 2016: Formal Methods, 2016, 748-756 p.Conference paper (Refereed)
The advanced technology used for developing modern automotive systems increases their complexity, making their correctness assurance very tedious. To enable analysis, but also enhance understanding and communication, by simulation, engineers use MATLAB/Simulink modeling during system development. In this paper, we provide further analysis means to industrial Simulink models by proposing a pattern-based, execution-order preserving transformation of Simulink blocks into the input language of UPPAAL Statistical Model checker, that is, timed (hybrid) automata with stochastic semantics. The approach leads to being able to analyze complex Simulink models of automotive systems, and we report our experience with two vehicular systems, the Brake-by-Wire and the Adjustable Speed Limiter.
Place, publisher, year, edition, pages
2016. 748-756 p.
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9995
Electrical Engineering, Electronic Engineering, Information Engineering
IdentifiersURN: urn:nbn:se:mdh:diva-33822DOI: 10.1007/978-3-319-48989-6_46ISI: 000389793300046ScopusID: 2-s2.0-84996523483ISBN: 978-3-319-48989-6 (print)OAI: oai:DiVA.org:mdh-33822DiVA: diva2:1048584
21st International Symposium on Formal Methods FM2016, 09 Nov 2016, Limassol, Cyprus
ProjectsVeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety