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
Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Mälardalen University.
Scania, Södertälje, Sweden.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-4987-7669
Show others and affiliations
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, Published 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.

Place, publisher, year, edition, pages
2016. Vol. 2, 167-173 p., 7552198
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-32866DOI: 10.1109/COMPSAC.2016.140ISI: 000389532200027Scopus ID: 2-s2.0-84987974300ISBN: 978-1-4673-8845-0 (print)OAI: oai:DiVA.org:mdh-32866DiVA: diva2:956954
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
In thesis
1. Pattern-based Specification and Formal Analysis of Embedded Systems Requirements and Behavioral Models
Open this publication in new window or tab >>Pattern-based Specification and Formal Analysis of Embedded Systems Requirements and Behavioral Models
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
pattern-based formal requirements specification, formal requirements consistency analysis, formal analysis of Simulink models
National Category
Engineering and Technology Computer and Information Science
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-35085 (URN)978-91-7485-319-3 (ISBN)
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-11-01Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Rodriguez-Navas, GuillermoSeceleanu, Cristina

Search in DiVA

By author/editor
Filipovikj, PredragRodriguez-Navas, GuillermoSeceleanu, Cristina
By organisation
Embedded SystemsMälardalen University
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 3 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