More Web Proxy on the site http://driver.im/

research-article

Evaluating model testing and model checking for finding requirements violations in Simulink models

Authors:

Khouloud Gaaloul,

Claudio Menghi,

Lionel C. Briand,

Stephen Foster,

David WolfeAuthors Info & Claims

ESEC/FSE 2019: Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Pages 1015 - 1025

https://doi.org/10.1145/3338906.3340444

Published: 12 August 2019 Publication History

Abstract

Matlab/Simulink is a development and simulation language that is widely used by the Cyber-Physical System (CPS) industry to model dynamical systems. There are two mainstream approaches to verify CPS Simulink models: model testing that attempts to identify failures in models by executing them for a number of sampled test inputs, and model checking that attempts to exhaustively check the correctness of models against some given formal properties. In this paper, we present an industrial Simulink model benchmark, provide a categorization of different model types in the benchmark, describe the recurring logical patterns in the model requirements, and discuss the results of applying model checking and model testing approaches to identify requirements violations in the benchmarked models. Based on the results, we discuss the strengths and weaknesses of model testing and model checking. Our results further suggest that model checking and model testing are complementary and by combining them, we can significantly enhance the capabilities of each of these approaches individually. We conclude by providing guidelines as to how the two approaches can be best applied together.

References

[1]

{n. d.}. Mathematica. https://www.wolfram.com/mathematica/. ({n. d.}). Accessed: 2019-04-26. 2019. Companion material. https://www.dropbox.com/sh/i9n764r1q6vjkxz/ AADsgN-gvX-ystJPMDVVjYhga?dl=0. (26 04 2019). 2019. qracorp. (2019). https://qracorp.com 2019. QVtrace. https://qracorp.com/qvtrace/. (01 02 2019).

[2]

Houssam Abbas, Georgios E. Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta. 2013. Probabilistic Temporal Logic Falsification of Cyber-Physical Systems. ACM Transactions on Embedded Computing Systems (TECS) 12, 2s (2013), 95:1–95:30.

Digital Library

[3]

Raja Ben Abdessalem, Shiva Nejati, Lionel C. Briand, and Thomas Stifter. 2016. Testing advanced driver assistance systems using multi-objective search and neural networks. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016. 63–74.

Digital Library

[4]

R. Alur. 2011. Formal verification of hybrid systems. In International Conference on Embedded Software (EMSOFT). 273–278.

Digital Library

[5]

Rajeev Alur. 2015. Principles of Cyber-Physical Systems. MIT Press.

[6]

Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A Henzinger, P-H Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. 1995. The algorithmic analysis of hybrid systems. Theoretical computer science 138, 1 (1995), 3–34.

Digital Library

[7]

Luciano Baresi, Marcio Delamaro, and Paulo Nardi. 2017. Test oracles for simulinklike models. Automated Software Engineering 24, 2 (2017), 369–391.

Digital Library

[8]

Jiri Barnat, Lubos Brim, Jan Beran, Tomas Kratochvila, and Italo R Oliveira. 2012. Executing model checking counterexamples in Simulink. In TASE 2012. IEEE, 245–248.

Digital Library

[9]

Lionel C. Briand, Shiva Nejati, Mehrdad Sabetzadeh, and Domenico Bianculli. 2016. Testing the untestable: model testing of complex software-intensive systems. In Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016 - Companion Volume. 789–792.

Digital Library

[10]

Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. 2001. Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19, 1 (2001), 7–34.

Digital Library

[11]

Edmund M Clarke and Paolo Zuliani. 2011. Statistical model checking for cyberphysical systems. In International Symposium on Automated Technology for Verification and Analysis. Springer, 1–12.

Digital Library

[12]

Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA, USA.

Digital Library

[13]

Rance Cleaveland, Scott A Smolka, and Steven T Sims. 2008. An instrumentationbased approach to controller model validation. In MDRAS 2008. Springer, 84–97.

Digital Library

[14]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). 337–340.

Digital Library

[15]

Alastair F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümmer. 2011. Software Verification Using k-Induction. In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings. 351–368.

Digital Library

[16]

Georgios E Fainekos and George J Pappas. 2009. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410, 42 (2009), 4262–4291.

Digital Library

[17]

Kerianne H. Gross, Aaron W. Fifarek, and Jonathan A. Hoffman. 2016. Incremental Formal Methods Based Design Approach Demonstrated on a Coupled Tanks Control System. In 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016, Orlando, FL, USA, January 7-9, 2016. 181–188.

Digital Library

[18]

Gregoire Hamon. 2008. Simulink Design Verifier - Applying Automated Formal Methods to Simulink and Stateflow. In AFM 2008. Citeseer.

[19]

Thomas A Henzinger, Peter W Kopke, Anuj Puri, and Pravin Varaiya. 1998. What’s decidable about hybrid automata? Journal of computer and system sciences 57, 1 (1998), 94–124.

Digital Library

[20]

Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CoRR abs/1702.01135 (2017). http://arxiv.org/abs/1702.01135

[21]

Kim G Larsen and Bent Thomsen. 1988. A modal process logic. In Logic in Computer Science. IEEE, 203–210.

[22]

Axel Legay, Benoît Delahaye, and Saddek Bensalem. 2010. Statistical model checking: An overview. In International Conference on Runtime Verification. Springer, 122–135.

Digital Library

[23]

Sean Luke. 2013. Essentials of Metaheuristics (second ed.). Lulu.

[24]

Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 152–166.

[25]

Reza Matinnejad, Shiva Nejati, Lionel Briand, and Thomas Bruckmann. 2018. Test Generation and Test Prioritization for Simulink Models with Dynamic Behavior. IEEE Transactions on Software Engineering (2018).

[26]

Reza Matinnejad, Shiva Nejati, and Lionel C. Briand. 2017. Automated testing of hybrid Simulink/Stateflow controllers: industrial case studies. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering (ESEC/FSE’17). 938–943.

Digital Library

[27]

Reza Matinnejad, Shiva Nejati, Lionel C. Briand, and Thomas Bruckmann. 2014. MiL testing of highly configurable continuous controllers: scalable search using surrogate models. In ACM/IEEE International Conference on Automated Software Engineering, ASE ’14, Vasteras, Sweden - September 15 - 19, 2014. 163–174.

Digital Library

[28]

Reza Matinnejad, Shiva Nejati, Lionel C. Briand, and Thomas Bruckmann. 2016. Automated Test Suite Generation for Time-continuous Simulink Models. In International Conference on Software Engineering (ICSE). ACM.

Digital Library

[29]

Reza Matinnejad, Shiva Nejati, Lionel C. Briand, Thomas Bruckmann, and Claude Poull. 2015. Search-based automated testing of continuous controllers: Framework, tool support, and case studies. Information & Software Technology 57 (2015), 705–722.

[30]

Phil McMinn. 2004. Search-based Software Test Data Generation: A Survey: Research Articles. Softw. Test. Verif. Reliab. 14, 2 (June 2004), 105–156.

Digital Library

[31]

Claudio Menghi, Shiva Nejati, Khouloud Gaaloul, and Lionel C. Briand. 2019. Generating Automated and Online Test Oracles for Simulink Models with Continuous and Uncertain Behaviors. CoRR abs/1903.03399 (2019). arXiv: 1903.03399 http://arxiv.org/abs/1903.03399

[32]

N. S. Nise. 2004. Control Systems Engineering (4th ed.). John-Wiely Sons.

Digital Library

[33]

Amir Pnueli. 1977. The temporal logic of programs. In Annual Symposium on Foundations of Computer Science (sfcs 1977). IEEE, 46–57.

Digital Library

[34]

Prover Technology. {n. d.}. Prover Plug-In Software. http://www.prover.com. ({n. d.}). {Online; accessed 17-Aug-2015}.

[35]

Reactive Systems Inc. 2010. Reactis Tester. http://www.reactive-systems.com/simulinktesting-validation.html. (2010). {Online; accessed 17-Aug-2015}.

[36]

The MathWorks Inc. {n. d.}. Simulink Design Verifier. http://nl.mathworks.com/ products/sldesignverifier/?refresh=true. ({n. d.}). {Online; accessed 17-Aug-2015}.

[37]

Håkan LS Younes and Reid G Simmons. 2006. Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation 204, 9 (2006), 1368–1409.

Digital Library

[38]

Justyna Zander, Ina Schieferdecker, and Pieter J Mosterman. 2012. Model-based testing for embedded systems. CRC Press.

Digital Library

[39]

Xi Zheng, Christine Julien, Miryung Kim, and Sarfraz Khurshid. 2017. Perceptions on the state of the art in verification and validation in cyber-physical systems. Systems Journal 11, 4 (2017), 2614–2627.

Cited By

Formica FFan TRajhans APantelic VLawford MMenghi C(2024)Simulation-Based Testing of Simulink Models With Test Sequence and Test Assessment BlocksIEEE Transactions on Software Engineering10.1109/TSE.2023.334375350:2(239-257)Online publication date: Mar-2024
https://doi.org/10.1109/TSE.2023.3343753
Luitel DNejati SSabetzadeh M(2024)Requirements-Driven Slicing of Simulink Models using LLMs2024 IEEE 32nd International Requirements Engineering Conference Workshops (REW)10.1109/REW61692.2024.00014(72-82)Online publication date: 24-Jun-2024
https://doi.org/10.1109/REW61692.2024.00014
Kröger JKoopmann BStierand IFränzle M(2024)Contract-based specification of mode-dependent timing behaviorInnovations in Systems and Software Engineering10.1007/s11334-023-00531-420:1(31-47)Online publication date: 1-Mar-2024
https://dl.acm.org/doi/10.1007/s11334-023-00531-4
Show More Cited By

Index Terms

Evaluating model testing and model checking for finding requirements violations in Simulink models
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Conditional model checking: a technique to pass information between verifiers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering

Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself ...
SMT-Based Model Checking of Industrial Simulink Models
Formal Methods and Software Engineering
Abstract
The development of embedded systems requires formal analysis of models such as those described with MATLAB/Simulink. However, the increasing complexity of industrial models makes analysis difficult. This paper proposes a model checking method for ...
Automatic test case generation from Simulink/Stateflow models using model checking

Model-based test generation techniques based on random input generation and guided simulation do not satisfy the demands of high test coverage and completeness guarantees as required by safety-critical applications. Recently, test generation techniques ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ESEC/FSE 2019: Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

August 2019

1264 pages

ISBN:9781450355728

DOI:10.1145/3338906

General Chairs:
Marlon Dumas
University of Tartu, Estonia
,
Dietmar Pfahl
University of Tartu, Estonia
,
Program Chairs:
Sven Apel
Saarland University, Germany
,
Alessandra Russo
Imperial College, UK

Copyright © 2019 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

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 August 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

European Research Council under the European Union?s Horizon 2020 research and innovation programme
Fonds National de la Recherche Luxembourg
Horizon 2020

Conference

ESEC/FSE '19

Sponsor:

SIGSOFT

ESEC/FSE '19: 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering

August 26 - 30, 2019

Tallinn, Estonia

Acceptance Rates

Overall Acceptance Rate 112 of 543 submissions, 21%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

34
Total Citations
View Citations
392
Total Downloads

Downloads (Last 12 months)44
Downloads (Last 6 weeks)6

Reflects downloads up to 28 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Formica FFan TRajhans APantelic VLawford MMenghi C(2024)Simulation-Based Testing of Simulink Models With Test Sequence and Test Assessment BlocksIEEE Transactions on Software Engineering10.1109/TSE.2023.334375350:2(239-257)Online publication date: Mar-2024
https://doi.org/10.1109/TSE.2023.3343753
Luitel DNejati SSabetzadeh M(2024)Requirements-Driven Slicing of Simulink Models using LLMs2024 IEEE 32nd International Requirements Engineering Conference Workshops (REW)10.1109/REW61692.2024.00014(72-82)Online publication date: 24-Jun-2024
https://doi.org/10.1109/REW61692.2024.00014
Kröger JKoopmann BStierand IFränzle M(2024)Contract-based specification of mode-dependent timing behaviorInnovations in Systems and Software Engineering10.1007/s11334-023-00531-420:1(31-47)Online publication date: 1-Mar-2024
https://dl.acm.org/doi/10.1007/s11334-023-00531-4
Boll AVieregg NKehrer T(2024)Replicability of experimental tool evaluations in model-based software and systems engineering with MATLAB/SimulinkInnovations in Systems and Software Engineering10.1007/s11334-022-00442-w20:3(209-224)Online publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1007/s11334-022-00442-w
Yang Y(2023)Improve Model Testing by Integrating Bounded Model Checking and Coverage Guided FuzzingElectronics10.3390/electronics1207157312:7(1573)Online publication date: 27-Mar-2023
https://doi.org/10.3390/electronics12071573
Jodat BChandar ANejati SSabetzadeh M(2023)Test Generation Strategies for Building Failure Models and Explaining Spurious FailuresACM Transactions on Software Engineering and Methodology10.1145/363824633:4(1-32)Online publication date: 21-Dec-2023
https://dl.acm.org/doi/10.1145/3638246
Mandrioli CShin SMaggio MBianculli DBriand L(2023)Stress Testing Control Loops in Cyber-physical SystemsACM Transactions on Software Engineering and Methodology10.1145/362474233:2(1-58)Online publication date: 20-Sep-2023
https://dl.acm.org/doi/10.1145/3624742
Mandrioli CNyberg Carlsson MMaggio M(2023)Testing Abstractions for Cyber-Physical Control SystemsACM Transactions on Software Engineering and Methodology10.1145/361717033:1(1-32)Online publication date: 23-Nov-2023
https://dl.acm.org/doi/10.1145/3617170
Arrieta AValle PAgirre JSagardui G(2023)Some Seeds Are Strong: Seeding Strategies for Search-based Test Case SelectionACM Transactions on Software Engineering and Methodology10.1145/353218232:1(1-47)Online publication date: 13-Feb-2023
https://dl.acm.org/doi/10.1145/3532182
Zhang ZLyu DArcaini PMa LHasuo IZhao J(2023)FalsifAI: Falsification of AI-Enabled Hybrid Control Systems Guided by Time-Aware Coverage CriteriaIEEE Transactions on Software Engineering10.1109/TSE.2022.319464049:4(1842-1859)Online publication date: 1-Apr-2023
https://doi.org/10.1109/TSE.2022.3194640
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