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
Quality Assurance for Dependable Embedded Systems
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-1844-7874
2018 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Architectural engineering of embedded computer systems comprehensively affects both the development processes and the abilities of the systems. Rigorous and holistic verification of architectural engineering is consequently essential in the development of safety-critical and mission-critical embedded systems, such as computer systems within aviation, automotive, and railway transportation, where even minor architectural defects may cause substantial cost and devastating harm. The increasing complexity of embedded systems renders this challenge unmanageable without the support of automated methods of verification, to reduce the cost of labor and the risk of human error.

The contribution of this thesis is an Architecture Quality Assurance Framework (AQAF) and a corresponding tool support, the Architecture Quality Assurance Tool (AQAT). AQAF provides a rigorous, holistic, and automated solution to the verification of critical embedded systems architectural engineering, from requirements analysis and design to implementation and maintenance. A rigorous and automated verification across the development process is achieved through the adaption and integration of formal methods to architectural engineering. The framework includes an architectural model checking technique for the detection of design faults, an architectural model-based test suite generation technique for the detection of implementation faults, and an architectural selective regression verification technique for an efficient detection of faults introduced by maintenance modifications.

An integrated solution provides traceability and coherency between the verification processes and the different artifacts under analysis, which is essential for obtaining reliable results, for meeting certification provisions, and for performing impact analyses of maintenance modifications. The Architecture Quality Assurance Tool (AQAT) implements the theory of AQAF and enables an effortless adoption into industrial practices. Empirical results from an industrial study present a high fault detection rate at both the design level and the implementation level as well as an efficient selective regression verification process. Furthermore, the results of a scalability evaluation show that the solution is scalable to complex many-core embedded systems with multithreading.

Place, publisher, year, edition, pages
Västerås: Mälardalen University Press , 2018.
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 252
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-37458ISBN: 978-91-7485-372-8 (print)OAI: oai:DiVA.org:mdh-37458DiVA, id: diva2:1166579
Public defence
2018-01-26, Gamma, Mälardalens högskola, Västerås, 13:00 (English)
Opponent
Supervisors
Available from: 2017-12-18 Created: 2017-12-15 Last updated: 2018-01-10Bibliographically approved
List of papers
1. An Architecture-Based Verification Technique for AADL Specifications
Open this publication in new window or tab >>An Architecture-Based Verification Technique for AADL Specifications
2011 (English)Conference paper, Published paper (Refereed)
Abstract [en]

Quality assurance processes of software-intensive systems are an increasing challenge as the complexity of these systems dramatically increases. The use of Architecture Description Languages (ADLs) provide an important basis for evaluation. The Architecture Analysis and Design Language (AADL) is an ADL developed for designing software intensive systems. In this paper, we propose an architecture-based verification technique covering the entire development process by adapting a combination of model-checking and model-based testing approaches to AADL specifications. The technique reveals inconsistencies of early design decisions and ensures a system's conformity with its AADL specification. The objective and criteria (test-selection) of the verification technique is derived from traditional integration testing.

Place, publisher, year, edition, pages
Berlin: Springer-Verlag, 2011
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6903
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-13590 (URN)000306397800011 ()
Conference
5th European Conference on Software Architecture (ECSA), Essen, Germany, 2011
Available from: 2011-12-15 Created: 2011-12-15 Last updated: 2017-12-15
2. Automated Verification of AADL-Specifications Using UPPAAL
Open this publication in new window or tab >>Automated Verification of AADL-Specifications Using UPPAAL
2012 (English)In: Proceedings of the 14th IEEE International Symposium on High Assurance Systems Engineering (HASE), 2012, p. 130-138Conference paper, Published paper (Refereed)
Abstract [en]

The Architecture Analysis and Design Language (AADL) is used to represent architecture design decisions of safety-critical and real-time embedded systems. Due to the far-reaching effects these decisions have on the development process, an architecture design fault is likely to have a significant deteriorating impact through the complete process. Automated fault avoidance of architecture design decisions therefore has the potential to significantly reduce the cost of the development while increasing the dependability of the end product. To provide means for automated fault avoidance when developing systems specified in AADL, a formal verification technique has been developed to ensure completeness and consistency of an AADL specification as well as its conformity with the end product. The approach requires the semantics of AADL to be formalized and implemented. We use the methodology of semantic anchoring to contribute with a formal and implemented semantics of a subset of AADL through a set of transformation rules to timed automata constructs. In addition, the verification technique, including the transformation rules, is validated using a case study of a safety-critical fuel-level system developed by a major vehicle manufacturer.

National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-17372 (URN)10.1109/HASE.2012.22 (DOI)2-s2.0-84871966304 (Scopus ID)978-1-4673-4742-6 (ISBN)
Conference
IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE), 25-27 Oct. 2012, Omaha, NE, USA
Available from: 2012-12-20 Created: 2012-12-20 Last updated: 2017-12-15Bibliographically approved
3. Regression verification of AADL models through slicing of system dependence graphs
Open this publication in new window or tab >>Regression verification of AADL models through slicing of system dependence graphs
2014 (English)In: QoSA 2014 - Proceedings of the 10th International ACM SIGSOFT Conference on Quality of Software Architectures (Part of CompArch 2014), 2014, p. 103-112Conference paper, Published paper (Refereed)
Abstract [en]

Design artifacts of embedded systems are subjected to a number of modifications during the development process. Verified artifacts that subsequently are modified must nec- essarily be re-Verified to ensure that no faults have been introduced in response to the modification. We collectively call this type of verification as regression verification. In this paper, we contribute with a technique for selective regression verification of embedded systems modeled in the Architec- ture Analysis and Design Language (AADL). The technique can be used with any AADL-based verification technique to eficiently perform regression verification by only selecting verification sequences that cover parts that are afiected by the modification for re-execution. This allows for the avoid- ance of unnecessary re-verification, and thereby unnecessary costs. The selection is based on the concept of specification slicing through system dependence graphs (SDGs) such that the efiect of a modification can be identified.

National Category
Computer Systems Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-25739 (URN)10.1145/2602576.2602589 (DOI)2-s2.0-84904459914 (Scopus ID)9781450325769 (ISBN)
Conference
10th International ACM SIGSOFT Conference on Quality of Software Architectures, QoSA 2014; Marcq-en-Baroeul; France; 30 June 2014 through 4 July 2014
Available from: 2014-08-01 Created: 2014-08-01 Last updated: 2018-01-11Bibliographically approved
4. AQAF: An architecture quality assurance framework for systems modeled in AADL
Open this publication in new window or tab >>AQAF: An architecture quality assurance framework for systems modeled in AADL
Show others...
2016 (English)In: Proceedings - 2016 12th International ACM SIGSOFT Conference on Quality of Software Architectures, QoSA 2016, 2016, p. 31-40Conference paper, Published paper (Refereed)
Abstract [en]

Architecture engineering is essential to achieve dependability of critical embedded systems and affects large parts of the system life cycle. There is consequently little room for faults, which may cause substantial costs and devastating harm. Verification in architecture engineering should therefore be holistically and systematically managed in the development of critical embedded systems, from requirements analysis and design to implementation and maintenance. In this paper, we address this problem by presenting AQAF: an Architecture Quality Assurance Framework for critical embedded systems modeled in the Architecture Analysis and Design Language (AADL). The framework provides a holistic set of verification techniques with a common formalism and semantic domain, architecture flow graphs and timed automata, enabling completely formal and automated verification processes covering virtually the entire life cycle. The effectiveness and efficiency of the framework are validated in a case study comprising a safety-critical train control system. 

Keywords
AADL, Architecture-based verification framework, Model checking, Model-based testing, Regression verification, Flow graphs, Java programming language, Life cycle, Quality assurance, Quality control, Safety engineering, Semantics, Architecture analysis and design language (AADL), Architecture engineering, Automated verification, Effectiveness and efficiencies, Model based testing, Verification framework, Verification techniques, Embedded systems
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-34462 (URN)10.1109/QoSA.2016.9 (DOI)000390444300004 ()2-s2.0-84983443358 (Scopus ID)9781509025671 (ISBN)
Conference
12th International ACM SIGSOFT Conference on Quality of Software Architectures, QoSA 2016, 5 April 2016 through 8 April 2016
Available from: 2016-12-20 Created: 2016-12-20 Last updated: 2017-12-15Bibliographically approved
5. AQAT: The Architecture Quality Assurance Tool for Critical Embedded Systems
Open this publication in new window or tab >>AQAT: The Architecture Quality Assurance Tool for Critical Embedded Systems
2017 (English)In: Proceedings - International Symposium on Software Reliability Engineering, ISSRE, Volume 2017, 2017, p. 260-270, article id 8109092Conference paper, Published paper (Refereed)
Abstract [en]

Architectural engineering of embedded systems comprehensively affects both the development processes and the abilities of the systems. Verification of architectural engineering is consequently essential in the development of safety- and mission-critical embedded system to avoid costly and hazardous faults. In this paper, we present the Architecture Quality Assurance Tool (AQAT), an application program developed to provide a holistic, formal, and automatic verification process for architectural engineering of critical embedded systems. AQAT includes architectural model checking, model-based testing, and selective regression verification features to effectively and efficiently detect design faults, implementation faults, and faults created by maintenance modifications. Furthermore, the tool includes a feature that analyzes architectural dependencies, which in addition to providing essential information for impact analyzes of architectural design changes may be used for hazard analysis, such as the identification of potential error propagations, common cause failures, and single point failures. Overviews of both the graphical user interface and the back-end processes of AQAT are presented with a sensor-to-actuator system example.

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-37453 (URN)10.1109/ISSRE.2017.32 (DOI)000426939700025 ()2-s2.0-85040780004 (Scopus ID)9781538609415 (ISBN)
Conference
28th IEEE International Symposium on Software Reliability Engineering, ISSRE 2017; Toulouse; France; 23 October 2017 through 26 October 2017
Available from: 2017-12-14 Created: 2017-12-14 Last updated: 2018-03-29Bibliographically approved
6. Experience Report: Evaluating Fault Detection Effectiveness and Resource Efficiency of the Architecture Quality Assurance Framework and Tool
Open this publication in new window or tab >>Experience Report: Evaluating Fault Detection Effectiveness and Resource Efficiency of the Architecture Quality Assurance Framework and Tool
Show others...
2017 (English)In: Proceedings - International Symposium on Software Reliability Engineering, ISSRE. Volume 2017, 2017, p. 271-281, article id 8109093Conference paper, Published paper (Refereed)
Abstract [en]

The Architecture Quality Assurance Framework (AQAF) is a theory developed to provide a holistic and formal verification process for architectural engineering of critical embedded systems. AQAF encompasses integrated architectural model checking, model-based testing, and selective regression verification techniques to achieve this goal. The Architecture Quality Assurance Tool (AQAT) implements the theory of AQAF and enables automated application of the framework. In this paper, we present an evaluation of AQAT and the underlying AQAF theory by means of an industrial case study, where resource efficiency and fault detection effectiveness are the targeted properties of evaluation. The method of fault injection is utilized to guarantee coverage of fault types and to generate a data sample size adequate for statistical analysis. We discovered important areas of improvement in this study, which required further development of the framework before satisfactory results could be achieved. The final results present a 100% fault detection rate at the design level, a 98.5% fault detection rate at the implementation level, and an average increased efficiency of 6.4% with the aid of the selective regression verification technique.

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-37457 (URN)10.1109/ISSRE.2017.31 (DOI)000426939700026 ()2-s2.0-85040780151 (Scopus ID)9781538609415 (ISBN)
Conference
28th International Symposium on Software Reliability Engineering (ISSRE), Toulouse, France, 2017
Available from: 2017-12-14 Created: 2017-12-14 Last updated: 2018-07-25Bibliographically approved

Open Access in DiVA

fulltext(5299 kB)51 downloads
File information
File name FULLTEXT02.pdfFile size 5299 kBChecksum SHA-512
b696f7c018db3bb7ef6bc613c73f4693f9c6f5bd6bb5cb4c7591199297cf205a742d4c2a1db3f82a6ef908ef604f78984316284666f9a6ea5bc7862b904eac4d
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Johnsen, Andreas
By organisation
Embedded Systems
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

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