This content is not included in your SAE MOBILUS subscription, or you are not logged in.
Formal Verification in Model Based Development
ISSN: 0148-7191, e-ISSN: 2688-3627
Published April 14, 2015 by SAE International in United States
Annotation ability available
Software verification is a critical component of software development. Software verification techniques include different forms of testing, inspection, static analysis, and formal verification. Formal verification offers the advantage that it corresponds, at least informally, to testing all possible paths through the software.
There are two primary approaches to using formal verification to establish properties of software: (a) proving properties of a formal specification, and (b) proving an implementation is a refinement of its specification. The first approach allows inference of the proven properties of the implementation provided the implementation is correct. The second approach allows inference of the correctness of the implementation.
Proving properties of a specification provides a means for detecting critical design flaws early in the development process. In model-based development, the model (e.g., a set of SIMULINK diagrams) is a formal specification of the desired system. Thus, formal methods can be applied to such models to gain the advantage of early defect detection.
The technique we have developed begins by synthesizing a formal specification of a SIMULINK model in the PVS specification language. Once the model has been converted to PVS, standard theorems that characterize the basic type and consistency rules of SIMULINK are proved using the PVS verification system.
Once the standard theorems are proved, theorems describing crucial properties (especially those related to safety) of the subject system are stated and proved. To demonstrate the utility and feasibility of our approach, we analyzed a hypothetical ABS controller model, based on a model provided by MathWorks.
CitationHocking, A., Knight, J., Aiello, M., and Shiraishi, S., "Formal Verification in Model Based Development," SAE Technical Paper 2015-01-0260, 2015, https://doi.org/10.4271/2015-01-0260.
- Strunk , Elisabeth A. , Yin Xiang , and Knight John C. Echo: a practical approach to formal verification Proceedings of the 10th international workshop on Formal methods for industrial critical systems 44 53 ACM 2005 10.1145/1081180.1081187
- Fitzgerald , John , Bicarregui Juan , Larsen Peter Gorm , and Woodcock Jim Industrial Deployment of Formal Methods: Trends and Challenges Industrial Deployment of System Engineering Methods 2014 10.1007/978-3-642-33170-1_10
- Brinkmann , Raik When failure is not an option in automotive verification 2014 http://www.techdesignforums.com/practice/technique/iso-26262-asil-formal-verification/ January 12 2015
- Amey , Peter Correctness by Construction: Better can also be Cheaper CrossTalk: the Journal of Defense Software Engineering 2 2002 24 28
- Woodcock , Jim , Larsen Peter Gorm , Bicarregui Juan , and Fitzgerald John Formal methods: Practice and experience ACM Computing Surveys (CSUR) 41 4 2009 19 10.1145/1592434.1592436
- AdaCore GNAT Pro chosen for UK's next-generation ATC system 2007 http://www.adacore.com/customers/uks-next-generation-atc-system/ October 14 2014
- Hocking , Ashlie B. , Knight John , Aiello M. Anthony , and Shiraishi Shin'ichi Proving Model Equivalence in Model Based Design 2014 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW) 2014 10.1109/ISSREW.2014.83
- Bouissou , Olivier and Chapoutot Alexandre An Operational Semantics for Simulink's Simulation Engine ACM SIGPLAN Notices 47 5 2012 129 138 10.1145/2248418.2248437
- SRI International PVS specification and verification system 2014 December 18 2014
- Owre , Sam , Shankar Natarajan , Rushby John M. , and Stringer-Calvert David W. J. PVS Language Reference Technical Report November 2001
- MathWorks Automotive Advisory Board Control Algorithm Modeling Guidelines Using MATLAB, Simulink, and Stateflow - Version 3.0 The MathWorks Automotive Advisory Board August 31 2012 http://www.mathworks.com/solutions/automotive/standards/docs/MAAB_Style_Guideline_Version3p00_pdf.zip October 14 2014
- Owre , Sam , Shankar Natarajan , Rushby John M. , and Stringer-Calvert David W. J. PVS System Guide Technical Report November 2001
- MathWorks Modeling an Anti-Lock Braking System Modeling an Anti-Lock Braking System September 20 2014 http://www.mathworks.com/help/simulink/examples/modelingan-anti-lock-braking-system.html October 14 2014
- MathWorks Simulink Design Verifier Simulink Design Verifier http://www.mathworks.com/products/sldesignverifier October 14 2014
- Alparslan , Denizhan Simulink Design Verifier 2.0 Product Presentation 2011 http://cmacs.cs.cmu.edu/presentations/verif_csystems/10_Deniz hanAlparslan.pdf October 14 2014
- MathWorks Simulink Verification and Validation: Verify models and generated code 2012 http://www.mathworks.com/products/datasheets/pdf/simulinkverification-and-validation.pdf October 14 2014
- MathWorks Static analysis with Polyspace products 2013 http://www.mathworks.com/products/polyspace October 14 2014
- MathWorks SystemTest: Manage tests and analyze results for system verification and validation 2013 http://www.mathworks.com/help/systemtest October 14 2014
- Esterel Technologies SCADE Suite Gateway for Simulink 2013 http://www.esterel-technologies.com/products/scadesuite/gateways/scade-suite-gateway-simulink October 14 2014
- Esterel Technologies SCADE Suite Design Verifier (DV) 2013 http://www.esterel-technologies.com/products/scadesuite/verify/design-verifier October 14 2014
- Reactive Systems, Inc. Testing and Validation of Simulink Models with Reactis November 2010 http://www.reactivesystems. com/simulink-testing-validation.html October 14 2014
- Zuliani , Paolo , Platzer André , and Clarke Edmund M. Bayesian Statistical Model Checking with Application to Simulink/Stateflow verification Proceedings of the 13th ACM international conference on Hybrid systems: computation and control 243 252 ACM 2010 10.1145/1755952.1755987
- Roy , Pritam , and Shankar Natarajan SimCheck: An Expressive Type System for Simulink NASA Formal Methods 149 160 2010
- James , Mark LDRA Extends Integration with MATLAB and Simulink, Verifying the Model at Object Code Level March 29 2013 http://www.ldra.com/attachments/article/131/LDRA_Mathworks_Integration_290312_UK.pdf October 14 2014
- Miller , Steven , Anderson Elise , Wagner Lucas , Whalen Michael , and Heimdahl Matts Formal verification of flight critical software Proceedings of the AIAA Guidance, Navigation and Control Conference and Exhibit 15 18 2005 10.2514/6.2005-6431