mdh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Automated Approaches for Formal Verification of Embedded Systems Artifacts
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. (Formal Modeling and Analysis of Embedded Systems)
2019 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Västerås: Mälardalen University , 2019.
Serie
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 292
Nyckelord [en]
embedded systems, Simulink, systems specifications, model-checking, formal verification
Nationell ämneskategori
Datorsystem
Forskningsämne
datavetenskap
Identifikatorer
URN: urn:nbn:se:mdh:diva-43408ISBN: 978-91-7485-429-9 (tryckt)OAI: oai:DiVA.org:mdh-43408DiVA, id: diva2:1314699
Disputation
2019-06-17, Gamma, Mälardalens högskola, Västerås, 13:30 (Engelska)
Opponent
Handledare
Projekt
VeriSpecTillgänglig från: 2019-05-09 Skapad: 2019-05-09 Senast uppdaterad: 2019-05-15Bibliografiskt granskad
Delarbeten
1. Reassessing the Pattern-Based Approach for Formalizing Requirements in the Automotive Domain
Öppna denna publikation i ny flik eller fönster >>Reassessing the Pattern-Based Approach for Formalizing Requirements in the Automotive Domain
2014 (Engelska)Ingår i: 2014 IEEE 22ND INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE (RE), IEEE , 2014, s. 444-450Konferensbidrag (Refereegranskat)
Abstract [en]

The importance of using formal methods and techniques for verification of requirements in the automotive industry has been greatly emphasized with the introduction of the new ISO26262 standard for road vehicles functional safety. The lack of support for formal modeling of requirements still represents an obstacle for the adoption of the formal methods in industry. This paper presents a case study that has been conducted in order to evaluate the difficulties inherent to the process of transforming the system requirements from their traditional written form into semi-formal notation. The case study focuses on a set of non-structured functional requirements for the Electrical and Electronic (E/E) systems inside heavy road vehicles, written in natural language, and reassesses the applicability of the extended Specification Pattern System (SPS) represented in a restricted English grammar. Correlating this experience with former studies, we observe that, as previously claimed, the concept of patterns is likely to be generally applicable for the automotive domain. Additionally, we have identified some potential difficulties in the transformation process, which were not reported by the previous studies and will be used as a basis for further research.

Ort, förlag, år, upplaga, sidor
IEEE, 2014
Serie
Proceedings of International Requirements Engineering, ISSN 1097-0592
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:mdh:diva-38376 (URN)000363280400055 ()978-1-4799-3033-3 (ISBN)
Konferens
IEEE 22nd International Requirements Engineering Conference (RE), AUG 25-29, 2014, Blekinge Inst Technol, Karlskrona, SWEDEN
Tillgänglig från: 2018-02-12 Skapad: 2018-02-12 Senast uppdaterad: 2019-05-09Bibliografiskt granskad
2. Automated SMT-based Consistency Checking of Industrial Critical Requirements
Öppna denna publikation i ny flik eller fönster >>Automated SMT-based Consistency Checking of Industrial Critical Requirements
2017 (Engelska)Ingår i: ACM SIGAPP Applied Computing Review, ISSN 1559-6915, E-ISSN 1931-0161, Vol. 17, nr 4, s. 15-28Artikel i tidskrift (Refereegranskat) 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.

Ort, förlag, år, upplaga, sidor
United States: ACM, 2017
Nyckelord
Requirements Consistency Analysis, Formal Methods, SMT, Z3
Nationell ämneskategori
Datorsystem
Identifikatorer
urn:nbn:se:mdh:diva-38940 (URN)000424075800002 ()
Projekt
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Tillgänglig från: 2018-05-15 Skapad: 2018-05-15 Senast uppdaterad: 2019-05-09Bibliografiskt granskad
3. Bounded Invariance Checking of Simulink Models
Öppna denna publikation i ny flik eller fönster >>Bounded Invariance Checking of Simulink Models
2019 (Engelska)Ingår i: Proceedings of the ACM Symposium on Applied Computing, 2019, Vol. Part F147772, s. 2168-2177Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

Currently, Simulink models can be verified rigorously against design errors or statistical properties. In this paper, we show how Simulink models can be formally analyzed against invariance properties using bounded model checking reduced to satisfiability modulo theories solving. In its basic form, the technique provides means for verification of an underlying model over bounded traces rigorously, however, in general the procedure is incomplete. We identify common Simulink block types and compositions by analyzing selected industrial models, and we show that for some of them the set of non-repeating states (reachability diameter) can be visited with a finite set of paths of finite length, yielding the verification complete. We complement our approach with a tool, called SyMC that automates the following: i) calculation of the reachability diameter size for some of the designs, ii) generation of finite (bounded) paths of the underlying Simulink model and their encoding into SMT-LIB format and iii) checking invariance properties using the Z3 SMT solver. To show the applicability of our approach, we apply it on a prototype implementation of an industrial Simulink model, namely Brake by Wire from Volvo Group Trucks Technology, Sweden. 

Nationell ämneskategori
Datorsystem
Identifikatorer
urn:nbn:se:mdh:diva-42803 (URN)10.1145/3297280.3297493 (DOI)000474685800302 ()2-s2.0-85065663281 (Scopus ID)
Konferens
SAC2019: The 34th ACM/SIGAPP Symposium On Applied Computing, Limassol, Cyprus, April 8-12, 2019
Tillgänglig från: 2019-02-27 Skapad: 2019-02-27 Senast uppdaterad: 2019-10-11Bibliografiskt granskad
4. Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners
Öppna denna publikation i ny flik eller fönster >>Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners
2019 (Engelska)Ingår i: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering2019, 2019, s. 92-103Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

With the ever-increasing size and complexity of the industrial software systems there is an imperative need for an automated, systematic and exhaustive verification of various software artifacts, such as system specifications, models, code, etc. A potential remedy for this need might lie in a pool of techniques for computer-aided verification of software related artifacts, including system specifications. The Achilles' heel of these techniques, and the main hinder for their wider adoption in industrial development process are the complexity and the specialized skill-set required for the formal encoding of specifications. To alleviate this problem, Specification Patterns that are based on the observation that the system specifications are framed within reoccurring solutions have been proposed. The approach has been shown to be expressive enough for capturing requirements in the automotive domain, however, there is a lack of empirical data that can be used to judge its practical usefulness. In this paper, we involve an existing specification-patterns-based tool, and propose a small-size evaluation of the approach with practitioners, on a case study conducted in cooperation with Scania, one of the world's leading manufacturers of heavy-load vehicles. Our results show that the specification patterns that are supported by an adequate tooling have the potential for adoption in industrial practice. 

Nationell ämneskategori
Datorsystem
Identifikatorer
urn:nbn:se:mdh:diva-42802 (URN)2-s2.0-85067481667 (Scopus ID)9789897583759 (ISBN)
Konferens
ENASE 2019: 14th International Conference on Evaluation of Novel Approaches to Software Engineering, Heraklion, Crete, Greece, May 4, 2019 - May 5, 2019
Tillgänglig från: 2019-02-27 Skapad: 2019-02-27 Senast uppdaterad: 2019-06-27Bibliografiskt granskad

Open Access i DiVA

fulltext(1317 kB)57 nedladdningar
Filinformation
Filnamn FULLTEXT02.pdfFilstorlek 1317 kBChecksumma SHA-512
5f6211680e4675fd9794f691909898b42e6d3fbc221904abb77cb4ce0d0a0611952c55b1699e7af694c06761bf3c6b6d7b564c9f5dd878a47372a27e492bf0d2
Typ fulltextMimetyp application/pdf

Personposter BETA

Filipovikj, Predrag

Sök vidare i DiVA

Av författaren/redaktören
Filipovikj, Predrag
Av organisationen
Inbyggda system
Datorsystem

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 57 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

isbn
urn-nbn

Altmetricpoäng

isbn
urn-nbn
Totalt: 372 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf