mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Pattern-based Specification and Formal Analysis of Embedded Systems Requirements and Behavioral Models
Mälardalen University, School of Innovation, Design and Engineering. (Formal Modeling and Analysis of Embedded Systems)
2017 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Since the first lines of code were introduced in the automotive domain, vehicles have transitioned from being predominantly mechanical systems to software intensive systems. With the ever-increasing computational power and memory of vehicular embedded systems, a set of new, more powerful and more complex software functions are installed into vehicles to realize core functionalities. This trend impacts all phases of the system development including requirements specification, design and architecture of the system, as well as the integration and testing phases. In such settings, creating and managing different artifacts during the system development process by using traditional, human-intensive techniques becomes increasingly difficult. One problem stems from the high number and intricacy of system requirements that combine functional and possibly timing or other types of constraints. Another problem is related to the fact that industrial development relies on models, e.g. developed in Simulink, from which code may be generated, so the correctness of such models needs to be ensured. A potential way to address of the mentioned problems is by applying computer-aided specification, analysis and verification techniques already at the requirements stage, but also further at later development stages. Despite the high degree of automation, exhaustiveness and rigor of formal specification and analysis techniques, their integration with industrial practice remains a challenge.

To address this challenge, in this thesis, we develop the foundation of a framework, tailored for industrial adoption, for formal specification and analysis of system requirements specifications and behavioral system models. First, we study the expressiveness of existing pattern-based techniques for creating formal requirements specifications, on a relevant industrial case study. Next, in order to enable practitioners to create formal system specification by using pattern-based techniques, we propose a tool called SeSAMM Specifier. Further, we provide an automated Satisfiability Modulo Theories (SMT)-based consistency analysis approach for the formally encoded system requirements specifications. The proposed SMT-based approach is suitable for early phases of the development for debugging the specifications. For the formal analysis of behavioral models, we provide an approach for statistical model checking of Simulink models by using the UPPAAL SMC tool. To facilitate the adoption of the approach, we provide the SIMPPAAL tool that automates procedure of generating network of stochastic timed automata for a given Simulink model. For validation, we apply our approach on a complex industrial model, namely the Brake-by-Wire function from Volvo GTT.

Place, publisher, year, edition, pages
Mälardalen University Press , 2017.
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 256
Keyword [en]
pattern-based formal requirements specification, formal requirements consistency analysis, formal analysis of Simulink models
National Category
Engineering and Technology
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-35085ISBN: 978-91-7485-319-3 (print)OAI: oai:DiVA.org:mdh-35085DiVA: diva2:1085177
Presentation
2017-04-20, Gamma, Högskoleplan 1, Västerås, 13:15 (English)
Opponent
Supervisors
Projects
VeriSpec
Funder
VINNOVA, 16335
Available from: 2017-03-28 Created: 2017-03-28 Last updated: 2017-07-10Bibliographically approved
List of papers
1. 2014 IEEE 22nd International Requirements Engineering Conference, RE 2014 - Proceedings
Open this publication in new window or tab >>2014 IEEE 22nd International Requirements Engineering Conference, RE 2014 - Proceedings
2014 (English)In: 2014 IEEE 22nd International Requirements Engineering Conference, RE 2014 - Proceedings, 2014, 444-450 p.Conference paper, (Refereed)
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.

Series
2014 IEEE 22nd International Requirements Engineering Conference, RE 2014 - Proceedings
Keyword
Automotive domains
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-26653 (URN)10.1109/RE.2014.6912296 (DOI)2-s2.0-84909947301 (Scopus ID)9781479930333 (ISBN)
Conference
2014 IEEE 22nd International Requirements Engineering Conference, RE 2014, 25 August 2014 through 29 August 2014
Available from: 2014-11-28 Created: 2014-11-28 Last updated: 2017-03-28Bibliographically approved
2. Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain
Open this publication in new window or tab >>Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain
Show others...
2016 (English)In: PROCEEDINGS 2016 IEEE 40TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSAC), VOL 2, 2016, Vol. 2, 167-173 p., 7552198Conference paper, (Refereed)
Abstract [en]

The lack of formal system specifications is a major obstacle to the widespread adoption of formal verification techniques in industrial settings. Specification patterns represent a promising approach that can fill this gap by enabling non-expert practitioners to write formal specifications based on reusing solutions to commonly occurring problems. Despite the fact that the specification patterns have been proven suitable for specification of industrial systems, there is no engineer-friendly tool support adequate for industrial adoption. In this paper, we present a tool called SESAMM Specifier in which we integrate a subset of the specification patterns for formal requirements specification, called SPS, into an existing industrial tool-chain. The tool provides the necessary means for the formal specification of system requirements and the later validation of the formally expressed behavior.

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-32866 (URN)10.1109/COMPSAC.2016.140 (DOI)000389532200027 ()2-s2.0-84987974300 (Scopus ID)978-1-4673-8845-0 (ISBN)
Conference
2016 IEEE 40th Annual Computer Software and Applications Conference, COMPSAC 2016; Atlanta; United States; 10 June 2016 through 14 June 2016; Category numberE5831; Code 123590
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2016-08-31 Created: 2016-08-24 Last updated: 2017-03-28Bibliographically approved
3. SMT-based Consistency Analysis of Industrial Systems Requirements
Open this publication in new window or tab >>SMT-based Consistency Analysis of Industrial Systems Requirements
2017 (English)In: 32nd ACM SIGAPP Symposium On Applied Computing SAC2017, 2017, Vol. F128005, 1272-1279 p.Conference paper, (Refereed)
Keyword
Con-sistency analysis, SMT, Specification patterns, System requirements, TCTL, Z3
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-34092 (URN)10.1145/3019612.3019787 (DOI)2-s2.0-85020883869 (Scopus ID)
Conference
32nd ACM SIGAPP Symposium On Applied Computing SAC2017, 03 Apr 2017, Marrakesh, Morocco
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2016-12-14 Created: 2016-12-13 Last updated: 2017-07-06Bibliographically approved
4. Analyzing Industrial Simulink Models by Statistical Model Checking
Open this publication in new window or tab >>Analyzing Industrial Simulink Models by Statistical Model Checking
Show others...
2017 (English)Report (Other academic)
Abstract [en]

The evolution of automotive systems has been rapid. Nowadays, electronic brains control dozens of functions in vehicles, like braking, cruising, etc. Model-based design approaches, in environments such as MATLAB Simulink, seem to help in addressing the ever-increasing need to enhance quality, and manage complexity, by supporting functional design from predefined block libraries, which can be simulated and analyzed for hidden errors, but also used for code generation. For this reason, providing assurance that Simulink models fulfill given functional and timing requirements is desirable. In this paper, we propose a pattern-based, execution-order preserving automatic transformation of Simulink atomic and composite blocks into stochastic timed automata that can then be analyzed formally with UPPAAL Statistical Model Checker (UPPPAAL SMC). Our method is supported by the tool SIMPPAAL, which we also introduce and apply on an industrial prototype called the Brake-by-Wire system. This work enables the formal analysis of industrial Simulink models, by automatically generating their semantic counterpart.

Place, publisher, year, edition, pages
Västerås, Sweden: Mälardalen Real-Time Research Centre, Mälardalen University, 2017
Series
MRTC Reports, ISSN 1404-3041
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-35069 (URN)MDH-MRTC-316/2017-1-SE (ISRN)
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2017-03-27 Created: 2017-03-27 Last updated: 2017-03-29Bibliographically approved

Open Access in DiVA

fulltext(1063 kB)7 downloads
File information
File name FULLTEXT03.pdfFile size 1063 kBChecksum SHA-512
50099e71c179b3385dc41b953bc3e53d4b3c5024d7f29b073a877c2bf2409857c8a2c50340a66b3e94fe06006fd77655bcaea0d34348d81645dec0415ed51c64
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Filipovikj, Predrag
By organisation
School of Innovation, Design and Engineering
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 7 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 287 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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