Automated test generation and error localisation for Simulink/Stateflow modelled systems using extended automata. Issue 1 (1st December 2016)

• Record Type: Journal Article
• Authors: Li, Meng; Kumar, Ratnesh
• Is Part Of: IET cyber-physical systems. Volume 1:Issue 1(2016)
• Page Start: 95
• Page End: 107
• Publication Date: 2016-12-01
• Subjects: program testing -- formal verification -- constraint handling -- finite automata -- cyber‐physical systems; automated test generation approach -- error localisation -- Model‐based development frameworks -- cyber‐physical systems -- model‐based CPS designs -- input‐output extended finite automata -- I/O‐EFA model -- model checking -- constraint solving
• DOI: 10.1049/iet-cps.2016.0024
• Languages: English
• ISSNs: 2398-3396

Abstract

Abstract : Model‐based development frameworks for cyber‐physical systems (CPSs) such as Simulink and Stateflow are popular for many applications. For safety and security concerns, verification and testing/validation must be performed on the model‐based CPS designs. In this study, the authors present an automatic test generation approach for model‐based CPS designs in Simulink/Stateflow based on its translation to input/output extended finite automata (I/O‐EFA) developed in the authors' prior works. The test generation problem requires identifying the executable paths of the I/O‐EFA model and also generating a test input for those paths. To execute a path, a certain sequence of other paths must be executed first, which they automatically identify. The approach is implemented by applying two different techniques, model checking and constraint solving. Both test generation implementations are validated by a case study. The results show that both implementations can generate test cases, while the implementation based on constraint solving is in general faster. The approach is further extended to requirements‐based test generation. These tests are then used for validation purposes, and the failed versus passed tests are used to localise the fault to plausible Simulink/Stateflow blocks using the notion of fault‐seed used in their earlier work. The approaches are applied on a bounded counter and a thermal control of a house as two different case studies.