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
Automated SMT-based Consistency Checking of Industrial Critical Requirements
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-4987-7669
Scania AB CV, Södertälje, Sweden.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
2017 (English)In: ACM SIGAPP Applied Computing Review, ISSN 1559-6915, E-ISSN 1931-0161, Vol. 17, no 4, p. 15-28Article in journal (Refereed) Published
Abstract [en]

With the ever-increasing size, complexity and intricacy of system requirements specifications, it becomes difficult to ensure their correctness with respect to certain criteria such as consistency. Automated formal techniques for consistency checking of requirements, mostly by means of model checking, have been proposed in academia. Sometimes such techniques incur a high modeling cost or analysis time, or are not applicable. To address such problems, in this paper we propose an automated consistency analysis technique of requirements that are formalized based on patterns, and checked using state-of-the-art Satisfiability Modulo Theories solvers. Our method assumes several transformation steps, from textual requirements to formal logic, and next into the format suited for the SMT tool. To automate such steps, we propose a tool, called PROPAS, that does not require any user intervention during the transformation and analysis phases, thus making the consistency analysis usable by non-expert practitioners. For validation, we apply our method on a set of timed computation tree logic requirements of an industrial automotive system called the Fuel Level Display.

Place, publisher, year, edition, pages
United States: ACM , 2017. Vol. 17, no 4, p. 15-28
Keywords [en]
Requirements Consistency Analysis, Formal Methods, SMT, Z3
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-38940ISI: 000424075800002OAI: oai:DiVA.org:mdh-38940DiVA, id: diva2:1205974
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional SafetyAvailable from: 2018-05-15 Created: 2018-05-15 Last updated: 2019-05-09Bibliographically approved
In thesis
1. Automated Approaches for Formal Verification of Embedded Systems Artifacts
Open this publication in new window or tab >>Automated Approaches for Formal Verification of Embedded Systems Artifacts
2019 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Modern embedded software is so large and complex that creating the necessary artifacts, including system requirements specifications and design-time models, as well as assuring their correctness have become difficult to manage. One challenge stems from the high number and intricacy of system requirements that combine functional and possibly timing or other types of constraints, which make them hard to analyze. Another challenge is the quality assurance of various design-time models developed using Simulink as the de facto standard model-based development tool in the automotive domain, avionics domain, etc. Currently, the industrial state-of-practice resorts to simulation of Simulink models, which gives insight in the system’s behavior yet does not provide a high degree of assurance that the model behaves correctly. A potential way to address the aforementioned challenges is to apply computer-aided, mathematically-rigorous methods for specification, analysis and verification already at the requirements specification stage, but also at later development stages.

In this thesis, we propose a set of approaches for the formal specification, analysis and verification of system requirement specifications and design-time Simulink models, with particular focus on the automotive industry. Our contributions are as follows: first, we assess the expressiveness of an existing patternbased technique for the formal requirements specification on an operational system. Based on the positive findings, we deem the technique expressive enough to capture systems requirements in controlled natural language, from which formal counterparts can be automatically generated. To bring the approach closer to the practitioners we propose a tool, called PROPAS. Next, we propose an automated consistency analysis approach based on Satisfiability Modulo Theories for the system requirements specifications formally encoded as temporal logic formulas. The approach is implemented in our PROPAS tool and is suitable to analyze the lack of logical contradictions within the system specification, at early system development phases. Our next contribution addresses the formal analysis and verification of large Simulink models. First, we propose a pattern-based and execution-order-preserving approach for transforming Simulink models into networks of stochastic timed automata, which can be analyzed using the UPPAAL SMC tool that returns the probability that a property is satisfied by the model. For the automated generation of the analysis model, we propose the SIMPPAAL tool. Our second approach is based on bounded model checking and is suitable for checking invariance properties of Simulink models. Compared to the statistical model checking approach, the invariance checking is reduced to a satisfiability problem. In case of property violation, the procedure generates a counter-example execution trace, which can be used for refining the model. In the same work we show that there exist commonly-used design patterns in Simulink models, for which the verification result is complete. The approach is supported by our SYMC tool.

For validation of the specification patterns, and the PROPAS tool we perform a case-study evaluation with practitioners, in collaboration with our industrial partner Scania. The results show that the pattern-based approach and the PROPAS tool can be practically useful in industrial settings. We apply the statistical model-checking approach and the SIMPPAAL tool on two industrial use cases, namely Brake-by-Wire and Adjustable Speed Limiter from Volvo Group Trucks Technology, which yields encouraging results. Finally, we validate the bounded invariance-checking approach and the SYMC tool on the Brake-by-Wire system, where we demonstrate both complete and incomplete verification of invariance properties.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2019
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 292
Keywords
embedded systems, Simulink, systems specifications, model-checking, formal verification
National Category
Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-43408 (URN)978-91-7485-429-9 (ISBN)
Public defence
2019-06-17, Gamma, Mälardalens högskola, Västerås, 13:30 (English)
Opponent
Supervisors
Projects
VeriSpec
Available from: 2019-05-09 Created: 2019-05-09 Last updated: 2019-05-15Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records BETA

Filipovikj, PredragRodriguez-Navas, GuillermoSeceleanu, Cristina

Search in DiVA

By author/editor
Filipovikj, PredragRodriguez-Navas, GuillermoSeceleanu, Cristina
By organisation
Embedded Systems
In the same journal
ACM SIGAPP Applied Computing Review
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
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