This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Applying Design Verification Tools in Automotive Software V&V
Technical Paper
2011-01-0745
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
Design verification technology promises comprehensive analysis of design models against the specified properties, thereby overcoming the limitations of traditional simulation-based and testing-based approaches. It helps in detecting design bugs early, thereby reducing the software development cycle time and cost. In this paper, we present our experiences with three state-of-the-art design verification tools - Reactis Validator, Simulink Design Verifier and Embedded Validator - for Simulink/Stateflow models. We also identify some challenges in employing them in an industrial production environment. We also suggest some automation steps to ease the design verification effort.
Recommended Content
Authors
Citation
Chakrapani Rao, A., Rajeev, A., and Yeolekar, A., "Applying Design Verification Tools in Automotive Software V&V," SAE Technical Paper 2011-01-0745, 2011, https://doi.org/10.4271/2011-01-0745.Also In
References
- 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
- Sims, Steve Cleaveland, Rance Butts, Ken Ranville, Scott “Automated Validation of Software Models” Proceedings of IEEE International Conference on Automated Software Engineering 2001
- Eisler, Stefan Scheidler, Christian Josko, Bernhard Sandmann, Guido Stroop, Joachim “Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications” Proceedings of World Congress on Formal Methods 2005
- McMurran, Ross Rao, Arun Chakrapani Jones, Peter “Model Based Validation Techniques for Complex Control Systems” Proceedings of Hybrid Vehicle Conference 2006
- Rao, A. McMurran, R. Jones, R. “A Critical Analysis of Model-Based Formal Verification Efforts within the Automotive Industry,” SAE Int. J. Passeng. Cars - Electron. Electr. Syst. 1 1 77 83 2009 10.4271/2008-01-0220
- de Miranda, A. Nascimento, L. “Software Validation a Vital Activity for a Mature Product Development Organization,” SAE Technical Paper 2005-01-4168 2005 10.4271/2005-01-4168
- Gautam, N. Yadav, O. “Model Based Development and Auto Testing: A Robust Approach for Reliable Automotive Software Development,” SAE Technical Paper 2006-01-1420 2006 10.4271/2006-01-1420
- Vuli, P. Badalament, M. Jaikamal, V. “Maximizing Test Asset Re-Use across MiL, SiL, and HiL Development Platforms,” SAE Technical Paper 2010-01-0660 2010 10.4271/2010-01-0660
- Conrad, M. Friedman, J. Sandmann, G. “Verification and Validation According to IEC 61508: A Workflow to Facilitate the Development of High-Integrity Applications,” SAE Int. J. Commer. Veh. 2 2 274 279 2010 10.4271/2009-01-2929
- Bouali, A. Dion, B. “Formal Verification for Model-Based Development,” SAE Technical Paper 2005-01-0781 2005 10.4271/2005-01-0781
- Henzinger, Thomas A. “The Theory of Hybrid Automata” Proceedings of IEEE Symposium on Logic in Computer Science 1996
- Clarke, Edmund M. Grumberg, Orna Peled, Doron A. “Model Checking” The MIT Press 2000
- Cleaveland, Rance Smolka, Scott A. Sims, Steven T. “An Instrumentation-Based Approach to Controller Model Validation” Proceedings of Automotive Software Workshop 2006
- EASIS Project http://www.easis-online.org/
- Proceedings of the 1st User Meeting on the Theme: Use of Embedded Validator and Embedded Tester in Industry 2007
- IBM Rational DOORS http://www-01.ibm.com/software/awdtools/doors/
- Rhapsody UML http://www-01.ibm.com/software/rational/uml/
- Rhapsody ATG http://www.btc-es.de/index.php?lang=2&idcatside=10
- Safety Test Builder http://www.geensoft.com/en/article/safetytestbuilder/
- Embedded Tester http://www.btc-es.de/index.php?lang=2&idcatside=2
- T-VEC Tester http://www.t-vec.com/solutions/simulink.php
- Simulink http://www.mathworks.com/products/simulink/
- Stateflow http://www.mathworks.com/products/stateflow/
- SCADE http://www.esterel-technologies.com/products/scade-suite/
- ASCET http://www.etas.com/en/products/ascet software products.php
- Modeling Metric Tool http://www.mathworks.com/matlabcentral/fileexchange/5574
- Reactis http://www.reactive-systems.com/
- Simulink Design Verifier http://www.mathworks.com/products/sldesignverifier/
- Embedded Validator http://www.btc-es.de/index.php?lang=2&idcatside=5
- TargetLink http://www.dspaceinc.com/en/inc/home/products/sw/pcgs/targetli.cfm
- SCADE Suite Design Verifier http://www.esterel-technologies.com/products/scade-suite/add-on-modules/design-verifier
- SCADE Suite Gateway for Simulink http://www.esterel-technologies.com/products/scade-suite/SCADE-Suite-Tool-Chain-Integration-Modules/
- Frehse, Goran “PHAVer: Algorithmic Verification of Hybrid Systems past HyTech” Proceedings of Hybrid Systems: Computation and Control 2005
- Platzer, André Quesel, Jan-David “KeYmaera: A Hybrid Theorem Prover for Hybrid Systems” Proceedings of International Joint Conference on Automated Reasoning 2008
- HybridSAL http://sal.csl.sri.com/hybridsal