mdh.sePublikasjoner
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.ORCID-id: 0000-0003-2870-2680
2019 (engelsk)Inngår i: ENASE 2019 - Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering2019, 2019, s. 92-103Konferansepaper, Publicerat paper (Fagfellevurdert)
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. 

sted, utgiver, år, opplag, sider
2019. s. 92-103
HSV kategori
Identifikatorer
URN: urn:nbn:se:mdh:diva-42802Scopus ID: 2-s2.0-85067481667ISBN: 9789897583759 (tryckt)OAI: oai:DiVA.org:mdh-42802DiVA, id: diva2:1292157
Konferanse
ENASE 2019: 14th International Conference on Evaluation of Novel Approaches to Software Engineering, Heraklion, Crete, Greece, May 4, 2019 - May 5, 2019
Tilgjengelig fra: 2019-02-27 Laget: 2019-02-27 Sist oppdatert: 2019-06-27bibliografisk kontrollert
Inngår i avhandling
1. Automated Approaches for Formal Verification of Embedded Systems Artifacts
Åpne denne publikasjonen i ny fane eller vindu >>Automated Approaches for Formal Verification of Embedded Systems Artifacts
2019 (engelsk)Doktoravhandling, med artikler (Annet vitenskapelig)
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.

sted, utgiver, år, opplag, sider
Västerås: Mälardalen University, 2019
Serie
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 292
Emneord
embedded systems, Simulink, systems specifications, model-checking, formal verification
HSV kategori
Forskningsprogram
datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-43408 (URN)978-91-7485-429-9 (ISBN)
Disputas
2019-06-17, Gamma, Mälardalens högskola, Västerås, 13:30 (engelsk)
Opponent
Veileder
Prosjekter
VeriSpec
Tilgjengelig fra: 2019-05-09 Laget: 2019-05-09 Sist oppdatert: 2019-05-15bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Scopus

Personposter BETA

Filipovikj, PredragSeceleanu, Cristina

Søk i DiVA

Av forfatter/redaktør
Filipovikj, PredragSeceleanu, Cristina
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric

isbn
urn-nbn
Totalt: 24 treff
RefereraExporteraLink to record
Permanent link

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