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
Ontology-based Analysis and Scalable Model Checking of Embedded Systems Models
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (Formal Modeling and Analysis of Embedded Systems)ORCID iD: 0000-0002-5626-0587
2017 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Currently, there is lack of effective and scalable methods to specify and ana-lyze requirements specifications, and verify the behavioral models of embed-ded systems. Most embedded systems requirements are expressed in naturallanguage which is flexible and intuitive but frequently ambiguous, vague andincomprehensive. Besides to natural language, template-based requirementsspecification methods are used to specify requirements specifications (esp. insafety-critical applications), which reduce ambiguity and improves the com-prehensibility of the specifications. However, the template-based method areusually rigid due to the fixed structures of the templates. They also lack meta-models for extensibility, and template selection is challenging.In this thesis, we proposed a domain specific language for embedded sys-tems, called ReSA, which is constrained natural language but flexible enoughto allow engineers to use different constructs to specify requirements. Thelanguage has formal semantics in proportional logic and description logic thatenables non-trivial and rigorous analysis of requirements specification, e.g.,consistency checking, completeness of specifications, etc.Moreover, we propose a scalable formal verification of Simulink models,whichisusedtodescribethebehaviorofsystemsthroughcommunicatingfunc-tional blocks. In industry, Simulink is the de facto modeling and analysis en-vironment of embedded systems. It is also used to generate code automati-cally from special Simulink models for various hardware platforms. However,Simulink lacks formal approach to verify large and hybrid Simulink models.Therefore, we also propose a formal verification of Simulink models, repre-sented as stochastic timed automata, using statistical model checking, whichhas proven to scale for industrial applications.We validate our approaches on industrial use cases from the automotiveindustry. These includes Adjustable Speed Limiter (ASL) and Brake-By-Wire(BBW) systems from Volvo Group Trucks Technology, both safety-critical.

Place, publisher, year, edition, pages
Västerås: Mälardalen University , 2017. , 200 p.
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 262
Keyword [en]
requirements specification, embedded systems, ontology, formal methods, simulink, sat, domain specific language, requirements boilerplates
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-35386ISBN: 978-91-7485-337-7 (print)OAI: oai:DiVA.org:mdh-35386DiVA: diva2:1098634
Presentation
2017-06-16, Gamma, Mälardalens högskola, Västerås, 13:15 (English)
Opponent
Supervisors
Projects
Verispec
Funder
VINNOVA, 16335
Available from: 2017-05-24 Created: 2017-05-24 Last updated: 2017-07-10Bibliographically approved
List of papers
1. ReSA Tool: Structured requirements specification and SAT-based consistency checking
Open this publication in new window or tab >>ReSA Tool: Structured requirements specification and SAT-based consistency checking
2016 (English)In: ReSA Tool: Structured requirements specification and SAT-based consistency-checking, 2016, 1737-1746 p.Conference paper, Published paper (Refereed)
Abstract [en]

Most industrial embedded systems requirements are specified in natural language, hence they can sometimes be ambiguous and error-prone. Moreover, employing an early-stage model-based incremental system development using multiple levels of abstraction, for instance via architectural languages such as EAST-ADL, calls for different granularity requirements specifications described with abstraction-specific concepts that reflect the respective abstraction level effectively. In this paper, we propose a toolchain for structured requirements specification in the ReSA language, which scales to multiple EAST-ADL levels of abstraction. Furthermore, we introduce a consistency function that is seamlessly integrated into the specification toolchain, for the automatic analysis of requirements logical consistency prior to their temporal logic formalization for full formal verification. The consistency check subsumes two parts: (i) transforming ReSA requirements specification into boolean expressions, and (ii) checking the consistency of the resulting boolean expressions by solving the satisfiability of their conjunction with the Z3 SMT solver. For validation, we apply the ReSA toolchain on an industrial vehicle speed control system, namely the Adjustable Speed Limiter.

Series
2016 Federated Conference on Computer Science and Information Systems (FedCSIS
Keyword
requirements specification, consistency checking, formal methods, embedded systems, automotive systems, software tool
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-34005 (URN)10.15439/2016F404 (DOI)000392436600246 ()2-s2.0-85007240246 (Scopus ID)978-8-3608-1090-3 (ISBN)
Conference
2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016; Gdansk; Poland; 11 September 2016 through 14 September 2016
Projects
VeriSpec
Funder
VINNOVA, 16335
Available from: 2016-11-29 Created: 2016-11-29 Last updated: 2017-05-24Bibliographically approved
2. ReSA: An Ontology-based Requirement Specification Language Tailored to Automotive Systems
Open this publication in new window or tab >>ReSA: An Ontology-based Requirement Specification Language Tailored to Automotive Systems
2015 (English)In: 2015 10th IEEE International Symposium on Industrial Embedded Systems (SIES), 2015, 1-10 p.Conference paper, Published paper (Refereed)
Abstract [en]

Automotive systems are developed using multi-leveled architectural abstractions in an attempt to manage the increasing complexity and criticality of automotive functions. Consequently, well-structured and unambiguously specified requirements are needed on all levels of abstraction, in order to enable early detection of possible design errors. However, automotive industry often relies on requirements specified in ambiguous natural language, sometimes in large and incomprehensible documents. Semi-formal requirements specification approaches (e.g., requirement boilerplates, pattern-based specifications, etc.) aim to reduce requirements ambiguity, without altering their readability and expressiveness. Nevertheless, such approaches do not offer support for specifying requirements in terms of multileveled architectural concepts, nor do they provide means for early-stage rigorous analysis of the specified requirements. In this paper, we propose a language, called ReSA, which allows requirements specification at various levels of abstraction, modeled in the architectural language of EAST-ADL. ReSA uses an automotive systems’ ontology that offers typing and syntactic axioms for the specification. Besides enforcing structure and more rigor in specifying requirements, our approach enables checking refinement as well as consistency of requirements, by proving ordinary boolean implications. To illustrate ReSA’s applicability, we show how to specify some requirements of the Adjustable Speed Limiter, which is a complex, safety-critical Volvo Trucks user function.

Keyword
automotive systems, requirements specification, boilerplates, ontology
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-29240 (URN)10.1109/SIES.2015.7185035 (DOI)000380569800001 ()2-s2.0-84959476620 (Scopus ID)978-1-4673-7711-9 (ISBN)
External cooperation:
Conference
10th IEEE International Symposium on Industrial Embedded Systems SIES'15, 8-10 Jun 2015, Siegen, Germany
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2015-10-06 Created: 2015-09-29 Last updated: 2017-05-24Bibliographically approved
3. Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Open this publication in new window or tab >>Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Show others...
2016 (English)In: FM 2016: Formal Methods, 2016, 748-756 p.Conference paper, Published paper (Refereed)
Abstract [en]

The advanced technology used for developing modern automotive systems increases their complexity, making their correctness assurance very tedious. To enable analysis, but also enhance understanding and communication, by simulation, engineers use MATLAB/Simulink modeling during system development. In this paper, we provide further analysis means to industrial Simulink models by proposing a pattern-based, execution-order preserving transformation of Simulink blocks into the input language of UPPAAL Statistical Model checker, that is, timed (hybrid) automata with stochastic semantics. The approach leads to being able to analyze complex Simulink models of automotive systems, and we report our experience with two vehicular systems, the Brake-by-Wire and the Adjustable Speed Limiter.

Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9995
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-33822 (URN)10.1007/978-3-319-48989-6_46 (DOI)000389793300046 ()2-s2.0-84996523483 (Scopus ID)978-3-319-48989-6 (ISBN)
Conference
21st International Symposium on Formal Methods FM2016, 09 Nov 2016, Limassol, Cyprus
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety
Available from: 2016-11-21 Created: 2016-11-21 Last updated: 2017-05-24Bibliographically approved

Open Access in DiVA

fulltext(1289 kB)31 downloads
File information
File name FULLTEXT02.pdfFile size 1289 kBChecksum SHA-512
c867db02c1f25e1084bfb11805d56594e823e0353327b857a359aa37d6140f46e201f18ec2c0d83752e89cca685637611dfaf44b78f1af172e912536d0764387
Type fulltextMimetype application/pdf

Authority records BETA

Mahmud, Nesredin

Search in DiVA

By author/editor
Mahmud, Nesredin
By organisation
Embedded Systems
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 31 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

isbn
urn-nbn

Altmetric score

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