This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Validation of Control Software Specification Using Design Interests Extraction and Model Checking
Technical Paper
2012-01-0960
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
Automotive control systems such as powertrain control interact with the open physical environment, and from this nature, expensive prototyping is indispensable to capture a deep understanding of the system requirements and to develop the corresponding control software. Model-based development (MBD) has been promoted to improve productivity by virtual prototyping. Even with MBD, systematic validation of the software specification remains as a major challenge and it still depends heavily on individual engineers' skill and knowledge. Though the introduction of graphical software modeling improved the situation, it requires much time to identify the primal functions, so-called “design interests”, from a large complex model where irrelevant components are mixed with, and to validate it properly. In addition, since software models have to coexist with legacy assets during the transition to MBD, the difficulty mentioned above should be overcome in terms of not only models, but also legacy C codes. As a remedy to this problem, we propose an approach based on design interests extraction from software model and/or legacy code. Design interests are mechanically extracted in the form of functional models and model checking is applied to exercise them. Currently, with our first tool implementation, a kind of dataflow graph is extracted from C codes as a functional model, and model checking is applied to prove specified properties on the dataflow graph and to generate execution traces which stimulate the specific parts of the design in a pinpoint manner. Such conditions are derived from the functional model.
Recommended Content
Technical Paper | Software-in-the-Loop Simulation Environment Realization using Matlab/Simulink |
Technical Paper | Model-Based Verification and Validation of Electronic Engine Controls |
Authors
Citation
Kaga, T., Adachi, M., Hosotani, I., and Konishi, M., "Validation of Control Software Specification Using Design Interests Extraction and Model Checking," SAE Technical Paper 2012-01-0960, 2012, https://doi.org/10.4271/2012-01-0960.Also In
References
- Clarke, E. Grumberg, O. Peled, D. “Model Checking” The MIT Press 0262032708 1999
- Ranville, S. “Case Study of Commercially Available Tools that Apply Formal Methods to a Matlab/Simulink/Stateflow Model,” SAE Technical Paper 2004-01-1765 2004 10.4271/2004-01-1765
- Chakrapani Rao, A. Rajeev, A. Yeolekar, A. “Applying Design Verification Tools in Automotive Software V&V,” SAE Technical Paper 2011-01-0745 2011 10.4271/2011-01-0745
- Coverity Static Analysis http://coverity.com/products/static-analysis.html
- CodeSonar http://www.grammatech.com/products/codesonar/overview.html
- CBMC http://www.cprover.org/cbmc/
- Clarke, E.M. Kroening, D. Lerda, F. “A Tool for Checking ANSI-C Programs” Tools and Algorithms for the Construction and Analysis of Systems 168 176 2004 10.1007/978-3-540-24730-2_15
- Aho, A. V. Sethi, R. Ullman, J. D. “Compilers” Addison Wesley 0201100886
- Ferrante, J. Ottenstein, K. J. Warren, J.D. “The program dependence graph and its use in optimization” ACM Transactions on Programming Languages and Systems (TOPLAS) 9 3 July 1987 10.1145/24039.24041
- Ammann, P. E. Black, P. E. Majurski, W. “Using Model Checking to Generate Tests from Specifications” Proceedings of the Second IEEE International Conference on Formal Engineering Methods (ICFEM'98) 46 54 1998 10.1109/ICFEM.1998.730569
- Holzer, A. Schallhart, C. Tautschnig, M. Veith, H. “FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement” CAV'08: Proceedings of the 20th international conference on Computer Aided Verification 209 213 2008 10.1007/978-3-540-70545_120
- Bizer, B. “Black box testing” Wiley 0471120944 1995