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
Model Checking-Based Software Testing for Function-Block Diagrams
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (Software Testing Laboratory)ORCID iD: 0000-0003-2416-4205
2014 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Software testing becomes more complex, more time-consuming, and more expensive. The risk that software errors remain undetected and cause critical failures increases. Consequently, in safety-critical development, testing software is standardized and it requires an engineer to show that tests fully exercise, or cover, the logic of the software. This method often requires a trained engineer to perform manual test generation, is prone to human error, and is expensive or impractical to use frequently in production. To overcome these issues, software testing needs to be performed earlier in the development process, more frequently, and aided by automated tools.

We devised an automated test generation tool called COMPLETETEST that avoids many of those problems. The method implemented in the tool and described in this thesis, works with software written in Function Block Diagram language, and can provide tests in just a few seconds. In addition, it does not rely on the expertise of a researcherspecialized in automated test generation and model checking. Although COMPLETETEST itself uses a model checker, a complex technique requiring a high level of expertise to generate tests, it provides a straightforward tabular interface to the intended users. In this way, its users do not need to learn the intricacies of using this approach such as how coverage criteria can be formalized and used by a model checker to automatically generate tests. If the technique can be demonstrated to work in production, it could detect and aid in the detection of errors in safety-critical software development, where conventional testing is not always applicable and efficient.

We conducted studies based on industrial use-case scenarios from Bombardier Transportation AB, showing how the approach can be applied to generate tests in software systems used in the safety-critical domain. To evaluate the approach, it was applied on real-world programs. The results indicate that it is efficient in terms of time required to generate tests and scales well for most of the software. There are still issues to resolve before the technique can be applied to more complex software, but we are already working on ways to overcome them. In particular, we need to understand how its usage in practice can vary depending on human and software process factors.

Place, publisher, year, edition, pages
Västerås: Mälardalen University , 2014.
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 182
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-26003ISBN: 978-91-7485-166-3 (print)OAI: oai:DiVA.org:mdh-26003DiVA: diva2:749702
Presentation
2014-11-07, Zeta, Västerås, 10:15 (English)
Opponent
Available from: 2014-09-25 Created: 2014-09-24 Last updated: 2014-11-03Bibliographically approved
List of papers
1. Model-based test suite generation for function block diagrams using the UPPAAL model checker
Open this publication in new window or tab >>Model-based test suite generation for function block diagrams using the UPPAAL model checker
2013 (English)In: Proceedings - IEEE 6th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2013, 2013, 158-167 p.Conference paper, (Refereed)
Abstract [en]

A method for model-based test generation of safety-critical embedded applications using Programmable Logic Controllers and implemented in a programming language such as Function Block Diagram (FBD) is described. The FBD component model is based on the IEC 1131 standard and it is used primarily for embedded systems, in which timeliness is an important property to be tested. Our method involves the transformation of FBD programs with timed annotations into timed automata models which are used to automatically generate test suites. Specifically we demonstrate how to use model transformation for formalization and model checking of FBD programs using the UPPAAL tool. Many benefits emerge from this method, including the ability to automatically generate test suites from a formal model in order to ensure compliance to strict quality requirements including unit testing and specific coverage measurements. The approach is experimentally assessed on a train control system in terms of consumed resources.

Keyword
function block diagram, model based testing, plc, structural coverage, test case generation, timed automata
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-21442 (URN)10.1109/ICSTW.2013.27 (DOI)000332185600028 ()2-s2.0-84883372535 (Scopus ID)
Conference
IEEE 6th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2013, 18 March 2013 through 20 March 2013, Luxembourg
Available from: 2013-09-13 Created: 2013-09-13 Last updated: 2015-11-13Bibliographically approved
2. Using Logic Coverage to Improve Testing Function Block Diagrams
Open this publication in new window or tab >>Using Logic Coverage to Improve Testing Function Block Diagrams
2013 (English)In: Testing Software and Systems: Lecture Notes in Computer Science, Volume 8254, Springer Berlin Heidelberg , 2013, 1-16 p.Chapter in book (Refereed)
Abstract [en]

In model-driven development, testers are often focusing on functional model-level testing, enabling verification of design models against their specifications. In addition, in safety-critical software development, testers are required to show that tests cover the structure of the implementation. Testing cost and time savings could be achieved if the process of deriving test cases for logic coverage is automated and provided test cases are ready to be executed. The logic coverage artifacts, i.e., predicates and clauses, are required for different logic coverage, e.g., MC/DC. One way of dealing with test case generation for ensuring logic coverage is to approach it as a model-checking problem, such that model-checking tools automatically create test cases. We show how logic coverage criteria can be formalized and used by a model-checker to provide test cases for ensuring this coverage on safety-critical software described in the Function Block Diagram programming language. Based on our experiments, this approach, supported by a tool chain, is an applicable and useful way of generating test cases for covering Function Block Diagrams.

Place, publisher, year, edition, pages
Springer Berlin Heidelberg, 2013
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8254
Keyword
logic coveragemodel-based testingfunction block diagramtimed automataIEC 61131-3test automation
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-22882 (URN)10.1007/978-3-642-41707-8_1 (DOI)2-s2.0-84893417933 (Scopus ID)978-3-642-41706-1 (ISBN)
Projects
ATAC - Advanced Test Automation for Complex Software-Intensive System (ITEA2/Vinnova)
Note

25th IFIP WG 6.1 International Conference, ICTSS 2013, Istanbul, Turkey, November 13-15, 2013, Proceedings

Available from: 2013-11-20 Created: 2013-11-19 Last updated: 2016-10-07Bibliographically approved
3. MOS: An Integrated Model-based and Search-based Testing Tool for Function Block Diagrams
Open this publication in new window or tab >>MOS: An Integrated Model-based and Search-based Testing Tool for Function Block Diagrams
Show others...
2013 (English)In: 2013 1st International Workshop on Combining Modelling and Search-Based Software Engineering, CMSBSE 2013 - Proceedings, 2013, 55-60 p.Conference paper, (Refereed)
Abstract [en]

In this paper we present a new testing tool for safety critical applications described in Function Block Diagram (FBD) language aimed to support both a model and a search-based approach. Many benefits emerge from this tool, including the ability to automatically generate test suites from an FBD program in order to comply to quality requirements such as component testing and specific coverage measurements. Search-based testing methods are used to generate test data based on executable code rather than the FBD program, alleviating any problems that may arise from the ambiguities that occur while creating FBD programs. Test cases generated by both approaches are executed and used as a way of cross validation. In the current work, we describe the architecture of the tool, its workflow process, and a case study in which the tool has been applied in a real industrial setting to test a train control management system.

National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-21334 (URN)10.1109/CMSBSE.2013.6605711 (DOI)2-s2.0-84886543950 (Scopus ID)978-1-4673-6284-9 (ISBN)
Conference
First International Workshop on Combining Modelling and Search-Based Software Engineering, 20th May 2013. In conjunction with ICSE 2013, San Francisco, California, USA
Projects
ATAC - Advanced Test Automation for Complex Software-Intensive System (ITEA2/Vinnova)ITS-EASY Post Graduate School for Embedded Software and Systems
Available from: 2013-09-19 Created: 2013-09-11 Last updated: 2015-11-13Bibliographically approved

Open Access in DiVA

fulltext(703 kB)463 downloads
File information
File name FULLTEXT02.pdfFile size 703 kBChecksum SHA-512
4419bc673568d4994a8c9a86b7070bd8c107b343346610bfdfdd48284279d50743ce3dc58196854e4191e73314464af66c9be99a07b1a67be5828da970bc238c
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Enoiu, Eduard
By organisation
Embedded Systems
Embedded Systems

Search outside of DiVA

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