Automatically finding bugs in a commercial cyber-physical system development tool chain with SLforge

ABSTRACT

Cyber-physical system (CPS) development tool chains are widely used in the design, simulation, and verification of CPS data-flow models. Commercial CPS tool chains such as MathWorks' Simulink generate artifacts such as code binaries that are widely deployed in embedded systems. Hardening such tool chains by testing is crucial since formally verifying them is currently infeasible. Existing differential testing frameworks such as CyFuzz can not generate models rich in language features, partly because these tool chains do not leverage the available informal Simulink specifications. Furthermore, no study of existing Simulink models is available, which could guide CyFuzz to generate realistic models.

To address these shortcomings, we created the first large collection of public Simulink models and used the collected models' properties to guide random model generation. To further guide model generation we systematically collected semi-formal Simulink specifications. In our experiments on several hundred models, the resulting SLforge generator was more effective and efficient than the state-of-the-art tool CyFuzz. SLforge also found 8 new confirmed bugs in Simulink.

References

1. H. Alemzadeh, R. K. Iyer, Z. Kalbarczyk, and J. Raman. 2013. Analysis of Safety-Critical Computer Failures in Medical Devices. IEEE Security Privacy 11, 4 (July 2013), 14--26.
2. Rajeev Alur. 2011. Formal verification of hybrid systems. InProc. 11th International Conference on Embedded Software, (EMSOFT) 2011. ACM, 273--278.
3. Rajeev Alur, Aditya Kanade, S. Ramesh, and K. C. Shashidhar. 2008. Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. In Proc. 8th ACM & IEEE International Conference on Embedded Software (EMSOFT). ACM, 89--98.
4. Stanley Bak, Sergiy Bogomolov, and Taylor T. Johnson. 2015. HYST: A Source Transformation and Translation Tool for Hybrid Automaton Models. In Proc. 18th International Conference on Hybrid Systems: Computation and Control (HSCC). ACM, 128--133.
5. Boris Beizer. 1990. Software testing techniques (second ed.). Van Nostrand Rein-hold.
6. Olivier Bouissou and Alexandre Chapoutot. 2012. An Operational Semantics for Simulink's Simulation Engine. In Proc. 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems (LCTES). ACM, 129--138.
7. Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer, and Georg Weissenbacher. 2009. Mutation-Based Test Case Generation for Simulink Models. In 8th International Symposium on Formal Methods for Components and Objects (FMCO). Springer, 208--227.
8. Junjie Chen, Wenxiang Hu, Dan Hao, Yingfei Xiong, Hongyu Zhang, Lu Zhang, and Bing Xie. 2016. An Empirical Comparison of Compiler Testing Techniques. In Proc. 38th International Conference on Software Engineering (ICSE). ACM, 180--190.
9. R. J. Chevance and T. Heidet. 1978. Static Profile and Dynamic Behavior of Cobol Programs. SIGPLAN Not. 13, 4 (April 1978), 44--57.
10. Shafiul Azam Chowdhury. 2018. Project Homepage. https://github.com/verivital/slsf_randgen/wiki. (2018). Accessed Feb 2018.
11. Shafiul Azam Chowdhury, Taylor T. Johnson, and Christoph Csallner. 2016. CyFuzz: A differential testing framework for cyber-physical systems development environments. In Proc. 6th Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy). Springer.
12. Christian S. Collberg, Ginger Myles, and Michael Stepp. 2007. An empirical study of Java bytecode programs. Softw., Pract. Exper. 37, 6 (2007), 581--641.
13. T.H. Cormen, C.E. Leiserson, R.L. Rivest, and C. Stein. 2001. Introduction To Algorithms. MIT Press.
14. Christoph Csallner and Yannis Smaragdakis. 2004. JCrasher: An automatic robustness tester for Java. Software---Practice & Experience 34, 11 (Sept. 2004), 1025--1050.
15. Yanja Dajsuren, Mark G.J. van den Brand, Alexander Serebrenik, and Serguei Roubtsov. 2013. Simulink Models Are Also Software: Modularity Assessment. In Proc. 9th International ACM SIGSOFT Conference on Quality of Software Architectures (QoSA). ACM, 99--106.
16. Florian Deissenboeck, Benjamin Hummel, Elmar Juergens, Michael Pfaehler, and Bernhard Schaetz. 2010. Model Clone Detection in Practice. In Proc. 4th International Workshop on Software Clones (IWSC). ACM, 57--64.
17. Kyle Dewey, Jared Roesch, and Ben Hardekopf. 2015. Fuzzing the Rust Type-checker Using CLP. In Proc. 30th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 482--493.
18. V. D'Silva, D. Kroening, and G. Weissenbacher. 2008. A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 27, 7 (July 2008), 1165--1178.
19. P. Fehér, T. Mészáros, L. Lengyel, and P. J. Mosterman. 2013. Data Type Propagation in Simulink Models with Graph Transformation. In Proc. 3rd Eastern European Regional Conference on the Engineering of Computer Based Systems. 127--137.
20. K. Ghani, J. A. Clark, and Y. Zhan. 2009. Comparing algorithms for search-based test data generation of Matlab Simulink models. In Proc. IEEE Congress on Evolutionary Computation. 2940--2947.
21. Antoine Girard, A. Agung Julius, and George J. Pappas. 2008. Approximate Simulation Relations for Hybrid Systems. Discrete Event Dynamic Systems 18, 2 (2008), 163--179.
22. Mark Grechanik, Collin McMillan, Luca DeFerrari, Marco Comi, Stefano Crespi, Denys Poshyvanyk, Chen Fu, Qing Xie, and Carlo Ghezzi. 2010. An Empirical Investigation into a Large-scale Java Open Source Code Repository. In Proc. ACM/IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM). ACM, 11:1--11:10.
23. C. Guger, A. Schlogl, C. Neuper, D. Walterspacher, T. Strein, and G. Pfurtscheller. 2001. Rapid prototyping of an EEG-based brain-computer interface (BCI). IEEE Transactions on Neural Systems and Rehabilitation Engineering 9, 1 (March 2001), 49--58.
24. Grégoire Hamon and John Rushby. 2007. An operational semantics for Stateflow. International Journal on Software Tools for Technology Transfer 9, 5 (2007), 447--456.
25. Christian Holler, Kim Herzig, and Andreas Zeller. 2012. Fuzzing with Code Fragments. In Proc. 21th USENIX Security Symposium. USENIX Association, 445--458. https://www.usenix.org/conference/usenixsecurity12/technical-sessions/presentation/holler
26. Ishtiaque Hussain, Christoph Csallner, Mark Grechanik, Qing Xie, Sangmin Park, Kunal Taneja, and B.M. Mainul Hossain. 2016. RUGRAT: Evaluating program analysis and testing tools and compilers with large generated random benchmark applications. Software---Practice & Experience 46, 3 (March 2016), 405--431.
27. Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts. 2017. Benchmarks for Model Transformations and Conformance Checking. https://cps-vo.org/node/12108. (2017). Accessed Feb 2018.
28. Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan, and K. C. Shashidhar. 2009. Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models. In Proc. 21st International Conference on Computer Aided Verification (CAV). Springer, 430--445.
29. Donald E. Knuth. 1971. An Empirical Study of FORTRAN Programs. Softw., Pract. Exper. 1, 2 (1971), 105--133.
30. Vu Le, Mehrdad Afshari, and Zhendong Su. 2014. Compiler validation via equivalence modulo inputs. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 216--226.
31. Christopher Lidbury, Andrei Lascu, Nathan Chong, and Alastair F. Donaldson. 2015. Many-core Compiler Fuzzing. In Proc. 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 65--76.
32. B. Liu, Lucia, S. Nejati, and L. C. Briand. 2017. Improving fault localization for Simulink models using search-based testing and prediction models. In Proc. 24th IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER). 359--370.
33. Reza Matinnejad, Shiva Nejati, Lionel C. Briand, and Thomas Bruckmann. 2016. SimCoTest: A test suite generation tool for Simulink/Stateflow controllers. In Proc. 38th International Conference on Software Engineering, (ICSE). ACM, 585--588.
34. William M. McKeeman. 1998. Differential Testing for Software. Digital Technical Journal 10, 1 (1998), 100--107. http://www.hpl.hp.com/hpjournal/dtj/vol10num1/vol10num1art9.pdf
35. Barton P. Miller, Louis Fredriksen, and Bryan So. 1990. An Empirical Study of the Reliability of Unix Utilities. Commun. ACM 33, 12 (Dec. 1990), 32--44.
36. M. Mohaqeqi and M. R. Mousavi. 2016. Sound Test-Suites for Cyber-Physical Systems. In 10th International Symposium on Theoretical Aspects of Software Engineering (TASE). 42--48.
37. Luan Viet Nguyen, Khaza Hoque, Stanley Bak, Steven Drager, and Taylor T. Johnson. 2018. Cyber-Physical Specification Mismatches. ACM Transactions on Cyber-Physical Systems (<a href="http://www.acm.org/TCPS/">TCPS</a>) (2018).
38. Luan Viet Nguyen, Christian Schilling, Sergiy Bogomolov, and Taylor T. Johnson. 2015. Runtime Verification of Model-based Development Environments. In Proc. 15th International Conference on Runtime Verification (RV).
39. Marta Olszewska, Yanja Dajsuren, Harald Altinger, Alexander Serebrenik, Marina A. Waldén, and Mark G. J. van den Brand. 2016. Tailoring complexity metrics for Simulink models. In Proc. 10th European Conference on Software Architecture Workshops. 5. http://dl.acm.org/citation.cfm?id=3004853
40. Vera Pantelic, Steven Postma, Mark Lawford, Monika Jaskolka, Bennett Mackenzie, Alexandre Korobkine, Marc Bender, Jeff Ong, Gordon Marks, and Alan Wassyng. 2017. Software engineering practices and Simulink: bridging the gap. International Journal on Software Tools for Technology Transfer (2017), 1--23.
41. N. H. Pham, H. A. Nguyen, T. T. Nguyen, J. M. Al-Kofahi, and T. N. Nguyen. 2009. Complete and accurate clone detection in graph-based models. In Proc. 31st IEEE International Conference on Software Engineering (ICSE). 276--286.
42. Pierre Giroux. 2018. Grid-Connected PV Array - File Exchange - Matlab Central. http://www.mathworks.com/matlabcentral/fileexchange/34752-grid-connected-pv-array. (Feb. 2018). Accessed Feb 2018.
43. A. C. Rajeev, Prahladavaradan Sampath, K. C. Shashidhar, and S. Ramesh. 2010. CoGenTe: A tool for code generator testing. In Proc. 25th IEEE/ACM International Conference on Automated Software Engineering (ASE). ACM, 349--350.
44. Steven Rasmussen, Jason Mitchell, Chris Schulz, Corey Schumacher, and Phillip Chandler. {n. d.}. A multiple UAV simulation for researchers. In AIAA Modeling and Simulation Technologies Conference and Exhibit. 5684.
45. Jesse Ruderman. 2007. Introducing jsfunfuzz. https://www.squarefree.com/2007/08/02/introducing-jsfunfuzz/. (2007). Accessed Feb 2018.
46. Prahladavaradan Sampath, A. C. Rajeev, S. Ramesh, and K. C. Shashidhar. 2007. Testing Model-Processing Tools for Embedded Systems. In Proc. 13th IEEE RealTime and Embedded Technology and Applications Symposium. IEEE, 203--214.
47. S. Sims, R. Cleaveland, K. Butts, and S. Ranville. 2001. Automated validation of software models. In Proc. 16th Annual International Conference on Automated Software Engineering (ASE). 91--96.
48. A. Sridhar, D. Srinivasulu, and D. P. Mohapatra. 2013. Model-based test-case generation for Simulink/Stateflow using dependency graph approach. In Proc. 3rd IEEE International Advance Computing Conference (IACC). 1414--1419.
49. Ingo Stürmer and Mirko Conrad. 2003. Test suite design for code generation tools. In Proc. 18th IEEE International Conference on Automated Software Engineering (ASE). 286--290.
50. Ingo Stürmer, Mirko Conrad, Heiko Dörr, and Peter Pepper. 2007. Systematic Testing of Model-Based Code Generators. IEEE Transactions on Software Engineering (TSE) 33, 9 (Sept. 2007), 622--634.
51. Giancarlo Succi, Witold Pedrycz, Snezana Djokic, Paolo Zuliani, and Barbara Russo. 2005. An Empirical Exploration of the Distributions of the Chidamber and Kemerer Object-Oriented Metrics Suite. Empirical Software Engineering 10, 1 (2005), 81--104.
52. E. Tempero, C. Anslow, J. Dietrich, T. Han, J. Li, M. Lumpe, H. Melton, and J. Noble. 2010. The Qualitas Corpus: A Curated Collection of Java Code for Empirical Studies. In 2010 Asia Pacific Software Engineering Conference. 336--345.
53. The MathWorks Inc. 2018. NASA HL-20 Lifting Body Airframe - Matlab & Simulink. https://www.mathworks.com/help/aeroblks/nasa-hl-20-lifting-body-airframe.html. (2018). Accessed Feb 2018.
54. The MathWorks Inc. 2018. Simulink Documentation. http://www.mathworks.com/help/simulink/. (2018). Accessed Feb 2018.
55. U.S. Consumer Product Safety Commission (CPSC). 2010. Recall 11-702: Fire Alarm Control Panels Recalled by Fire-Lite Alarms Due to Alert Failure. http://www.cpsc.gov/en/Recalls/2011/Fire-Alarm-Control-Panels-Recalled-by-Fire-Lite-Alarms-Due-to-Alert-Failure. (Oct. 2010). Accessed Feb 2018.
56. U.S. National Highway Traffic Safety Administration (NHTSA). 2014. Defect Information Report 14V-053. http://www-odi.nhtsa.dot.gov/acms/cs/jaxrs/download/doc/UCM450071/RCDNN-14V053-0945.pdf. (Feb. 2014).
57. U.S. National Institute of Standards and Technology (NIST). 2002. The economic impacts of inadequate infrastructure for software testing: Planning report 02-3. (May 2002).
58. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In Proc. 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 283--294.
59. Hongyu Zhang and Hee Beng Kuan Tan. 2007. An Empirical Study of Class Sizes for Large Java Systems. In Proc. 14th Asia-Pacific Software Engineering Conference (APSEC). 230--237.
60. Liang Zou, Naijun Zhan, Shuling Wang, and Martin Fränzle. 2015. Formal Verification of Simulink/Stateflow Diagrams. In Proc. 13th International Symposium on Automated Technology for Verification and Analysis (ATVA), Bernd Finkbeiner, Geguang Pu, and Lijun Zhang (Eds.). Springer, 464--481.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging

  • Software organization and properties

    • Software system structures

      • Software system models

        • Model-driven software engineering