This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Proving Properties of Simulink Models that Include Discrete Valued Functions
Technical Paper
2016-01-0129
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
For many crucial applications, establishing important properties of Simulink models by testing is either extremely resource intensive or impossible, and proof of the properties is highly desirable. Many Simulink models rely upon discrete-valued functions for which the function values are defined as a lookup table of correspondences between values in the domain and range, with linear interpolation used to evaluate intermediate values in the domain. Such discrete-valued functions arise in applications for which no known closed-form algebraic definition exists.
In general, the proof of a property for a model that includes a discrete-valued function has to be by case analysis. For a single function and with mechanical support, case analysis is manageable. However, for models that include multiple discrete-valued functions, the number of cases can be the product of the cardinalities of the domains of the individual functions. We have observed production models in which this product rises to a level in which proof is intractable using standard techniques.
In this paper, we examine four approaches to dealing with the combinatorial explosion: parallelism, pruning, approximation with flat-interpolated lookup tables, and functional approximation. For each approach, we discuss the concept and present a preliminary analysis of performance.
Authors
Citation
Hocking, A., Aiello, M., Knight, J., Shiraishi, S. et al., "Proving Properties of Simulink Models that Include Discrete Valued Functions," SAE Technical Paper 2016-01-0129, 2016, https://doi.org/10.4271/2016-01-0129.Also In
References
- Rushby , John. Critical system properties: Survey and taxonomy Reliability Engineering & System Safety 43 2 1994 189 219
- Gerhart , Susan , Craigen Dan , and Ralston Ted Experience with formal methods in critical systems High-Integrity System Specification and Design 2012 413
- RTCA/DO-178C Software Considerations in Airborne Systems and Equipment Certification December 13 2011
- Evans , David , and Larochelle David Improving security using extensible lightweight static analysis Software, IEEE 19.1 2002 42 51
- Moy , Yannick , Ledinot Emmanuel , Delseny Harvé , Wiels Virginia , and Monate Benjamin Testing or formal verification: DO-178C alternatives and industrial experience Software, IEEE 30.3 2013 50 57
- AdaCore GNAT Pro chosen for UK’s next-generation ATC system 2007 http://www.adacore.com/customers/uks-next-generation-atc-system/ October 16 2015
- Pieter Philippaerts , Mühlberg Jan Tobias , Penninckx Willem , Smans Jan , Jacobs Bart , and Piessens Frank Software verification with VeriFast: Industrial case studies Science of Computer Programming 82 2014 77 97
- MathWorks Simulink Verification and Validation: Verify models and generated code 2015 http://www.mathworks.com/products/simverification October 16 2015
- Esterel Technologies SCADE Suite Design Verifier (DV) 2014 http://www.esterel-technologies.com/products/scade-suite/verification-validation/scade-suite-design-verifier/ October 16 2015
- Reactive Systems, Inc. Testing and Validation of Simulink Models with Reactis October 2013 http://www.reactive-systems.com/simulink-testing-validation.html October 16 2015
- Hocking , Ashlie B. , Knight John , Aiello M. Anthony , and Shiraishi Shinichi Proving Model Equivalence in Model Based Design 2014 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW) 2014 10.1109/ISSREW.2014.83
- Hocking , A. , Knight , J. , Aiello , M. , and Shiraishi , S. Formal Verification in Model Based Development SAE Technical Paper 2015-01-0260 2015 10.4271/2015-01-0260