research-article

Localizing Faults in Simulink/Stateflow Models with STL

Authors:

Thomas Ferrère,

Niveditha Manjunath,

Dejan NičkovićAuthors Info & Claims

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 197 - 206

https://doi.org/10.1145/3178126.3178131

Published: 11 April 2018 Publication History

Abstract

Fault-localization is considered to be a very tedious and time-consuming activity in the design of complex Cyber-Physical Systems (CPS). This laborious task essentially requires expert knowledge of the system in order to discover the cause of the fault. In this context, we propose a new procedure that aids designers in debugging Simulink/Stateflow hybrid system models, guided by Signal Temporal Logic (STL) specifications. The proposed method relies on three main ingredients: (1) a monitoring and a trace diagnostics procedure that checks whether a tested behavior satisfies or violates an STL specification, localizes time segments and interfaces variables contributing to the property violations; (2) a slicing procedure that maps these observable behavior segments to the internal states and transitions of the Simulink model; and (3) a spectrum-based fault-localization method that combines the previous analysis from multiple tests to identify the internal states and/or transitions that are the most likely to explain the fault. We demonstrate the applicability of our approach on two Simulink models from the automotive and the avionics domain.

References

[1]

R. Abreu, P. Zoeteweij, and A. J. C. van Gemund. 2007. On the Accuracy of Spectrum-based Fault Localization. In Testing: Academic and Industrial Conference Practice and Research Techniques. IEEE, 89--98.

Digital Library

[2]

Yashwanth Annapureddy, Che Liu, Georgios E. Fainekos, and Sriram Sankaranarayanan. 2011. S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (LNCS), Vol. 6605. Springer, 254--257.

Digital Library

[3]

Shay Artzi, Julian Dolby, Frank Tip, and Marco Pistoia. 2010. Directed Test Generation for Effective Fault Localization. In International Symposium on Software Testing and Analysis. ACM, New York, NY, USA, 49--60.

Digital Library

[4]

Benoit Baudry, Franck Fleurey, and Yves Le Traon. 2006. Improving test suites for efficient fault localization. In International Conference on Software Engineering. ACM, 82--91.

Digital Library

[5]

Laurian Dinca and Tunc Aldemir. 1997. An On-Line Parameter Estimation Scheme for Fault Diagnosis. IFAC Proceedings Volumes 30, 18 (1997), 289--294.

[6]

Ram Das Diwakaran, Sriram Sankaranarayanan, and Ashutosh Trivedi. 2017. Analyzing neighborhoods of falsifying traces in cyber-physical systems. In International Conference on Cyber-Physical Systems. ACM, 109--119.

Digital Library

[7]

Alexandre Donzé. 2010. Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. In International Conference on Computer Aided Verification (LNCS), Vol. 6174. Springer, 167--170.

Digital Library

[8]

Thomas Ferrère, Oded Maler, and Dejan Nickovic. 2015. Trace Diagnostics Using Temporal Implicants. In International Symposium on Automated Technology for Verification and Analysis (LNCS), Vol. 9364. Springer, 241--258.

[9]

P.M. Frank and X. Ding. 1997. Survey of robust residual generation and evaluation methods in observer-based fault detection systems. Journal of Process Control 7, 6 (1997), 403--424.

[10]

Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo, Vasumathi Raman, Alexandre Donzé, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, and Sanjit A. Seshia. 2016. Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications. In International Conference on Hybrid Systems: Computation and Control. ACM, 31--40.

Digital Library

[11]

Bardh Hoxha, Houssam Abbas, and Georgios E. Fainekos. 2015. Benchmarks for Temporal Logic Requirements for Automotive Systems. In International Workshop on Applied veRification for Continuous and Hybrid Systems (EPiC Series in Computing), Vol. 34. EasyChair, 25--30.

[12]

James A. Jones and Mary Jean Harrold. 2005. Empirical Evaluation of the Tarantula Automatic Fault-Localization Technique. In International Conference on Automated Software Engineering. ACM, Long Beach, CA, USA, 273--282.

Digital Library

[13]

Ron Koymans. 1990. Specifying Real-Time Properties with Metric Temporal Logic. Real-Time Systems 2, 4 (1990), 255--299.

Digital Library

[14]

Bing Liu, Lucia, Shiva Nejati, and Lionel C. Briand. 2017. Improving fault localization for Simulink models using search-based testing and prediction models. In International Conference on Software Analysis, Evolution and Reengineering. IEEE Computer Society, 359--370.

[15]

Bing Liu, Lucia, Shiva Nejati, Lionel C. Briand, and Thomas Bruckmann. 2016. Localizing Multiple Faults in Simulink Models. In International Conference on Software Analysis, Evolution, and Reengineering. IEEE Computer Society, 146--156.

[16]

Bing Liu, Lucia, Shiva Nejati, Lionel C. Briand, and Thomas Bruckmann. 2016. Simulink fault localization: an iterative statistical debugging approach. Softw. Test., Verif. Reliab. 26, 6 (2016), 431--459.

[17]

Oded Maler and Dejan Ničković. 2013. Monitoring properties of analog and mixed-signal circuits. STTT 15, 3 (2013), 247--268.

Digital Library

[18]

Oded Maler, Dejan Ničković, and Amir Pnueli. 2008. Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday (LNCS), Vol. 4800. Springer, 475--505.

Digital Library

[19]

MathWorks. 2017. Isolating Problematic Behavior with Model Slicer. https://www.mathworks.com/products/sldesignverifier/features.html#isolating-problematic-behavior-with-model-slicer. (2017).

[20]

Pieter J. Mosterman and Jason Ghidella. 2006. Fault Detection Control Logic in an Aircraft Elevator Control System. https://www.mathworks.com/help/stateflow/examples/fault-detection-control-logic-in-an-aircraft-elevator-control-system.html. (2006).

[21]

Dejan Ničković and Oded Maler. 2007. AMT: A Property-Based Monitoring Tool for Analog Systems. In International Conference on Formal Modeling and Analysis of Timed Systems (LNCS), Vol. 4763. Springer, 304--319.

Digital Library

[22]

Joël Ouaknine, Alexander Rabinovich, and James Worrell. 2009. Time-Bounded Verification. In International Conference on Concurrency Theory (LNCS), Vol. 5710. Springer, 496--510.

Digital Library

[23]

Robert Reicherdt and Sabine Glesner. 2012. Slicing MATLAB Simulink models. In International Conference on Software Engineering. IEEE Computer Society, 551--561.

Digital Library

[24]

Jeremias Rößler, Gordon Fraser, Andreas Zeller, and Alessandro Orso. 2012. Isolating failure causes through test case generation. In International Symposium on Software Testing and Analysis. ACM, 309--319.

Digital Library

[25]

Sriram Sankaranarayanan and Georgios E. Fainekos. 2012. Falsification of temporal properties of hybrid systems using the cross-entropy method. In International Conference on Hybrid Systems: Computation and Control. ACM, 125--134.

Digital Library

[26]

W. Eric Wong, Ruizhi Gao, Yihao Li, Rui Abreu, and Franz Wotawa. 2016. A Survey on Software Fault Localization. IEEE Trans. Software Eng. 42, 8 (2016), 707--740.

Digital Library

[27]

Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy V. Deshmukh, James Kapinski, and Xiaoqing Jin. 2015. Falsification of safety properties for closed loop control systems. In International Conference on Hybrid Systems: Computation and Control. ACM, 299--300.

Digital Library

Cited By

Yadav DChristakis MPradel M(2024)From Fault Injection to Formal Verification: A Holistic Approach to Fault Diagnosis in Cyber-Physical SystemsProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685552(1896-1900)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685552
Zou YLi HLi DZhao MChen Z(2024)Systematic Analysis of Learning-Based Software Fault Localization2024 10th International Symposium on System Security, Safety, and Reliability (ISSSR)10.1109/ISSSR61934.2024.00068(478-489)Online publication date: 16-Mar-2024
https://doi.org/10.1109/ISSSR61934.2024.00068
Zhang ZAn JArcaini PHasuo I(2024)CauMon: An Informative Online Monitor for Signal Temporal LogicFormal Methods10.1007/978-3-031-71177-0_18(286-304)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_18
Show More Cited By

Index Terms

Localizing Faults in Simulink/Stateflow Models with STL
1. Computing methodologies
  1. Modeling and simulation
    1. Model development and analysis
      1. Model verification and validation
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Verifying simulink stateflow model: timed automata approach
ASE '16: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering

Simulink Stateflow is widely used for the model-driven development of software. However, the increasing demand of rigorous verification for safety critical applications brings new challenge to the Simulink Stateflow because of the lack of formal ...
Using SPIN to Check Nondeterministic Simulink Stateflow Models
ISMVL '15: Proceedings of the 2015 IEEE 45th International Symposium on Multiple-Valued Logic

In this paper, we consider model checking of nondeterministic finite state machine. Such a machine can be specified as a Simulink Stateflow model, but cannot be directly checked for properties such as reach ability. We present tool chains that use SPIN ...
Localizing faults using verification technique
Abstract
In model-based fault diagnosis, it is assumed that a correct model of each program being diagnosed is available. In general, these techniques require test cases and user-specified assertions to localize the fault. This paper aims to localize ...
Highlights
- The approach works for situations where calls to the recursive procedures are present.
- An example with loops is now incorporated.
- The tables are now updated with score and time.

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

April 2018

296 pages

ISBN:9781450356428

DOI:10.1145/3178126

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Research
Refereed limited

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
390
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)3

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yadav DChristakis MPradel M(2024)From Fault Injection to Formal Verification: A Holistic Approach to Fault Diagnosis in Cyber-Physical SystemsProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685552(1896-1900)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685552
Zou YLi HLi DZhao MChen Z(2024)Systematic Analysis of Learning-Based Software Fault Localization2024 10th International Symposium on System Security, Safety, and Reliability (ISSSR)10.1109/ISSSR61934.2024.00068(478-489)Online publication date: 16-Mar-2024
https://doi.org/10.1109/ISSSR61934.2024.00068
Zhang ZAn JArcaini PHasuo I(2024)CauMon: An Informative Online Monitor for Signal Temporal LogicFormal Methods10.1007/978-3-031-71177-0_18(286-304)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_18
Bartocci EMateis CNesterini ENičković D(2023)Mining Hyperproperties using Temporal LogicsACM Transactions on Embedded Computing Systems10.1145/360939422:5s(1-26)Online publication date: 31-Oct-2023
https://dl.acm.org/doi/10.1145/3609394
Nenzi LBartocci EBortolussi LSilvetti SLoreti M(2023)MoonLight: a lightweight tool for monitoring spatio-temporal propertiesInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-023-00710-525:4(503-517)Online publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1007/s10009-023-00710-5
Zhang ZAn JArcaini PHasuo I(2023)Online Causation Monitoring of Signal Temporal LogicComputer Aided Verification10.1007/978-3-031-37706-8_4(62-84)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_4
Lima LHerasimau ARaszyk MTraytel DYuan S(2023)Explainable Online Monitoring of Metric Temporal LogicTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30820-8_28(473-491)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30820-8_28
Leopold H(2023)Mastering Trustful Artificial IntelligenceResponsible Artificial Intelligence10.1007/978-3-031-09245-9_6(133-158)Online publication date: 2-Feb-2023
https://doi.org/10.1007/978-3-031-09245-9_6
Zhang ZArcaini PXie X(2022)Online Reset for Signal Temporal Logic MonitoringIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.319769341:11(4421-4432)Online publication date: Nov-2022
https://doi.org/10.1109/TCAD.2022.3197693
Bartocci EMariani LNickovic DYadav D(2022)Search-based Testing for Accurate Fault Localization in CPS2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE55969.2022.00024(145-156)Online publication date: Oct-2022
https://doi.org/10.1109/ISSRE55969.2022.00024
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten