mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-5626-0587
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-7663-5497
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
Show others and affiliations
2016 (English)In: FM 2016: Formal Methods, 2016, 748-756 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9995
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:mdh:diva-33822DOI: 10.1007/978-3-319-48989-6_46ISI: 000389793300046Scopus ID: 2-s2.0-84996523483ISBN: 978-3-319-48989-6 (print)OAI: oai:DiVA.org:mdh-33822DiVA: diva2:1048584
Conference
21st International Symposium on Formal Methods FM2016, 09 Nov 2016, Limassol, Cyprus
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2016-11-21 Created: 2016-11-21 Last updated: 2017-05-24Bibliographically approved
In thesis
1. Ontology-based Analysis and Scalable Model Checking of Embedded Systems Models
Open this publication in new window or tab >>Ontology-based Analysis and Scalable Model Checking of Embedded Systems Models
2017 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Currently, there is lack of effective and scalable methods to specify and ana-lyze requirements specifications, and verify the behavioral models of embed-ded systems. Most embedded systems requirements are expressed in naturallanguage which is flexible and intuitive but frequently ambiguous, vague andincomprehensive. Besides to natural language, template-based requirementsspecification methods are used to specify requirements specifications (esp. insafety-critical applications), which reduce ambiguity and improves the com-prehensibility of the specifications. However, the template-based method areusually rigid due to the fixed structures of the templates. They also lack meta-models for extensibility, and template selection is challenging.In this thesis, we proposed a domain specific language for embedded sys-tems, called ReSA, which is constrained natural language but flexible enoughto allow engineers to use different constructs to specify requirements. Thelanguage has formal semantics in proportional logic and description logic thatenables non-trivial and rigorous analysis of requirements specification, e.g.,consistency checking, completeness of specifications, etc.Moreover, we propose a scalable formal verification of Simulink models,whichisusedtodescribethebehaviorofsystemsthroughcommunicatingfunc-tional blocks. In industry, Simulink is the de facto modeling and analysis en-vironment of embedded systems. It is also used to generate code automati-cally from special Simulink models for various hardware platforms. However,Simulink lacks formal approach to verify large and hybrid Simulink models.Therefore, we also propose a formal verification of Simulink models, repre-sented as stochastic timed automata, using statistical model checking, whichhas proven to scale for industrial applications.We validate our approaches on industrial use cases from the automotiveindustry. These includes Adjustable Speed Limiter (ASL) and Brake-By-Wire(BBW) systems from Volvo Group Trucks Technology, both safety-critical.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2017. 200 p.
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 262
Keyword
requirements specification, embedded systems, ontology, formal methods, simulink, sat, domain specific language, requirements boilerplates
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-35386 (URN)978-91-7485-337-7 (ISBN)
Presentation
2017-06-16, Gamma, Mälardalens högskola, Västerås, 13:15 (English)
Opponent
Supervisors
Projects
Verispec
Funder
VINNOVA, 16335
Available from: 2017-05-24 Created: 2017-05-24 Last updated: 2017-07-10Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Filipovikj, PredragMahmud, NesredinMarinescu, RalucaSeceleanu, Cristina
By organisation
Embedded Systems
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 13 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf