This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Criteria-Driven Approach in Automotive Software Development – Integrating Concepts of Formal Methods with Testing
Technical Paper
2017-01-0003
ISSN: 0148-7191, e-ISSN: 2688-3627
This content contains downloadable datasets
Annotation ability available
Sector:
Language:
English
Abstract
We propose a verification method in the field of automotive control systems integrating the concepts of Formal Methods with testing, aiming at efficient and reliable software development. Although Formal Methods are believed to provide the benefits of their rigorous nature and their inherent capability of automation, only limited cases are known where Formal Methods were applied in system and software development, in practice, due to two major difficulties: appropriate abstraction in modeling and scalability in automated reasoning. Focusing on testing on the other hand, there is the difficulty of selecting reasonable set of tests for given verification objectives. In order to overcome these difficulties, our approach is to present verification criteria for testing to appropriately cover the property with the help of the Formal Method concepts. From the consistency with respect to the abstraction level of models between generic property (such as controllability) and underlying assumptions, we derive test coverage that covers the models and the assumptions. Based on a case study using a set of the artifact of a product system, we propose a criteria-driven approach with potential benefits in that we expect to gain the practical efficiency of testing the automotive control systems with the concept of model-checking.
Recommended Content
Authors
Citation
Tohdo, T., "Criteria-Driven Approach in Automotive Software Development – Integrating Concepts of Formal Methods with Testing," SAE Technical Paper 2017-01-0003, 2017, https://doi.org/10.4271/2017-01-0003.Data Sets - Support Documents
Title | Description | Download |
---|---|---|
Unnamed Dataset 1 |
Also In
References
- Gaudel , M.-C. Testing can be formal, too. In TAPSOFT'95 Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE Aarhus, Denmark May 22-26, 1995, Proceedings , P. Mosses , D. Nielsen M. , and Schwartzbach M. I. , Eds Lecture Notes in Computer Science 915 Springer Berlin, Heidelberg 82 96
- Grumberg and O . Long D. E. Model Checking and Modular Verification ACM Transactions on Programming Languages and Systems 16 843 872 May 1994
- Cofer , D.D. , Gacek , A. , Miller , S.P. , Whalen , M.W. , LaValley , B. , Sha , L. Compositional verification of architectural models Goodloe , A.E. , Person , S. , eds. Proceedings of the 4th NASA Formal Methods Symposium (NFM 2012) 7226 Berlin, Heidelberg Springer-Verlag 2012 126 140
- Benveniste , A . Caillaud , B . Nickovic , D . Passerone , R . Raclet , J.-B. Reinkemeier , P . Contracts for system design INRIA Rennes, France Tech. Rep. RR-8147 Nov 2012
- MathWorks Modeling an Automatic Transmission Controller https://www.mathworks.com/help/simulink/examples/modeling-an-automatic-transmission-controller.html Dec. 2016
- BTC Embedded Systems, User Documentation, BTC EmbeddedPlatform, Concepts and Use Cases, Release 2.0p1
- NuSMV: a new symbolic model checker http://nusmv.fbk.eu/ Dec 2016
- Pnueli A 1977 The Temporal Logic of Programs Foundations of Computer Science (FOCS) IEEE Computer Society Providence, Rhode Island, USA 46 57
- Baier and C . Katoen J.-P. Principles of Model Checking MIT Press 2007
- Benveniste , A . Caillaud , and B . Passerone , R A: generic model of contracts for embedded systems Rep. RR-6214 INRIA 2007
- McMillan , K.L. Circular Compositional Reasoning about Liveness Technical Report 999-02 Cadence Berkeley Labs Berkeley CA 1999
- Lamport L Formal foundation for specification and verification Distributed Systems: Methods and Tools for Specification, LNCS 190. Springer-Verlag 1985
- Chang and E . Manna and Z . Pnueli A The safety-progress classification Bauer F. L. , Brauer W. , and Schwichtenberg H. , editors Logic and Algebra of Specification, volume 94 of NATO ASI Series F: Computer and Systems Sciences 143 202 Springer-Verlag 1992
- Whalen , M. W. Rajan , A . Heimdahl , and M. P. Miller S. P. Coverage metrics for requirements-based testing ISSTA’06: Proceedings of the 2006 international symposium on Software testing and analysis 25 36 New York, NY, USA 2006 ACM Press
- Angelo Gargantini and Constance Heitmeyer Using Model Checking to Generate Tests From Requirements Specifications ESEC/FSE’99: 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, volume 1687 146 162 Springer September 1999
- Aichernig , B.K. , Brandl , H. , Jöbstl , E. , Krenn , W. , Schlick , R. , Tiran , S. Killing strategies for model-based mutation testing Software Testing, Verification and Reliability 2014
- Leucker , M. , Schallhart , C. A brief account of runtime verification Journal of Logic and Algebraic Programming 78 2008 293 303
- Sen , K . Marinov , and D . Agha G CUTE: A Concolic Unit Testing Engine for C Proceedings of the 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE’05) Lisbon, Portugal 2005 263 272