This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Application of Model Checking to Automotive Control Software with Slicing Technique
Technical Paper
2013-01-0436
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
To detect difficult-to-find defects in automotive control systems, we have proposed a modeling method with a program slicing technique. In this method, a verifier adjusts the boundaries of source code to be extracted on a variable dependence graph, in a kind of data flow. We have developed software tools for this method and achieved a 35% decrease in total verification time on model checking.
This paper provides some consideration on effective cases of the method from verification practices. There are two types of malfunction causes: one is the timing of processes (race conditions), and the other is complex logics. Each type requires different elements in external environment models. Furthermore, we propose regression verification based on the modeling method above, to further reduce verification time on model checking. The paper outlines tool extensions needed to realize regression verification.
Recommended Content
Technical Paper | Wire Harness Simulation and Analysis Techniques |
Technical Paper | Model-Based Software Technology Providing Safer Automotive Development and High Quality |
Technical Paper | Application of Model Fuels to Engine Simulation |
Authors
Citation
Matsubara, M., Sakurai, K., Narisawa, F., Enshoiwa, M. et al., "Application of Model Checking to Automotive Control Software with Slicing Technique," SAE Technical Paper 2013-01-0436, 2013, https://doi.org/10.4271/2013-01-0436.Also In
References
- Weiser , M. Program Slicing ICSE '81 Proceedings of the 5th international conference on Software engineering 439 449 1981
- Horwitz , S. , Reps , T. , and Binkley , D Interprocedural slicing using dependence graphs Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation 35 46 1988 10.1145/53990.5399
- Reps , T. , Horwitz , S. , Sagiv , M. and Rosay , G. Speeding up Slicing ACM SIGSOFT Software Engineering Notes 19 5 11 20 1994 10.1145/193173.195287
- Reps , T. and Rosay , G. Precise interprocedural chopping ACM SIGSOFT Software Engineering Notes 20 4 41 52 1995 10.1145/222124.222138
- Holzmann , G. J. The SPIN Model Checker Addison-Wesley Pub. 2003
- Holzmann , G.J. and Ruys , T.C. Effective Bug Hunting with SPIN and Modex Proceedings of the 12th International SPIN Workshop 2005 10.1007/11537328/_3
- Corbett , J. C. , Dwyer M. B. et al. Bandera: Extracting Finite-state Models from Java Source Code Proceedings of the 22nd International Conference on Software Engineering 2000 10.1109/ICSE.2000.870434
- Clarke , E. , Kroening , E. , and Lerda , F. A tool for checking ANSI-C programs Proceedings of Tools and Algorithms for the Construction and Analysis of Systems 2004 10.1007/978-3-540-24730-2/_15
- Beyer , D. , Henzinger , T. A. , Jhala , R. , Majumdar , R. The software model checker BLAST Journal on Software Tools for Technology Transfer 505 525 2007 10.1007/s10009-007-0044-z
- Ball , T. , Levin , V. , Rajamani , S. K. A Decade of Software Model Checking with SLAM Communications of the ACM 54 7 68 76 2011 10.1145/1965724.1965743
- Matsubara , M. , Sakurai , K. , Narisawa , F. , Enshoiwa , M. , Yamane , Y. , Yamanaka , H. Model Checking with Program Slicing Based on Variable Dependence Graph Proceedings of the 1th Formal Techniques for Safety-Critical Systems 2012 10.4204/EPTCS.105.5