research-article

Efficient safety checking for automotive operating systems using property-based slicing and constraint-based environment generation

Authors:

Dongwoo KimAuthors Info & Claims

Science of Computer Programming, Volume 103, Issue C

Pages 51 - 70

https://doi.org/10.1016/j.scico.2014.10.006

Published: 01 June 2015 Publication History

Abstract

We propose a collaborative safety checking method for automotive operating systems.Collaborative checking improves effectiveness of code-level safety checking.Property-based code slicing improves the efficiency of model checking and testing. An automotive operating system is a safety-critical system that has a critical impact on the safety of road vehicles. Safety verification is a must in each stage of software development in such a system, but most existing work focuses on specification-level or model-level safety verification. This work proposes a collaborative approach using model checking and testing for the efficient safety checking of an automotive operating system. Efficiency is achieved through property-based slicing, which reduces the complexity of verification, and guided test sequence generation, which limits the input space to a set of representative test sequences selected from legal as well as illegal input spaces. Comprehensiveness is achieved by formally specifying external constraints using constraint automata from which guided test sequences are selected. The approach is implemented as a prototype tool set applied to the verification of an open source automotive operating system based on the OSEK/VDX international standard. The approach revealed several safety issues that could not be identified by existing approaches.

References

[1]

M. Park, T. Byun, Y. Choi, Property-based code slicing for efficient verification of OSEK/VDX operating systems, in: EPTCS, vol. 105, 2012, pp. 69-84.

[2]

M. Broy, Challenges in automotive software engineering, in: 28th International Conference on Software Engineering, ACM, 2006, pp. 33-42.

Digital Library

[3]

J. Mössinger, Software in automotive systems, IEEE Softw., 27 (2010) 92-94.

Digital Library

[4]

E.M. Clarke, O. Grumberg, D. Peled, Model Checking, MIT Press, 1999.

[5]

G.J. Holzmann, The SPIN Model Checker - Primer and Reference Manual, Addison-Wesley Publishing Company, 2004.

[6]

E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst., 8 (1986) 244-263.

Digital Library

[7]

T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, Lazy abstraction, in: Proceedings of the 29th Symposium on Principles of Programming Languages, ACM, 2002, pp. 58-70.

[8]

G.J. Holzmann, M.H. Smith, An automated verification method for distributed systems software based on model extraction, IEEE Trans. Softw. Eng., 28 (2002) 364-377.

Digital Library

[9]

J.M. Cobleigh, G.S. Avrunin, L.A. Clarke, Breaking up is hard to do: an evaluation of automated assume-guarantee reasoning, ACM Trans. Softw. Eng. Methodol., 17 (2008) 1-52.

Digital Library

[10]

Y. Choi, Model checking Trampoline OS: a case study on safety analysis for automotive software, Softw. Test. Verif. Reliab., 24 (2014) 38-60.

[11]

D. Giannakopoulou, C.S. Pasareanu, H. Barringer, Assumption generation for software component verification, in: 17th IEEE International Conference on Automated Software Engineering, IEEE Computer Society, 2002, pp. 3-12.

[12]

N. Halbwachs, F. Lagnier, P. Raymond, Synchronous observers and the verification of reactive systems, in: Proceedings of the Third International Conference on Methodology and Software Technology, Workshops in Computing, Springer, 1993, pp. 83-96.

[13]

N. Ioustinova, N. Sidorova, M. Steffen, Abstraction and flow analysis for model checking open asynchronous systems, in: 9th Asia-Pacific Software Engineering Conference, IEEE Computer Society, 2002, pp. 227-235.

[14]

J. Penix, W. Visser, S. Park, C.S. Pasareanu, E. Engstrom, A. Larson, N. Weininger, Verifying time partitioning in the DEOS scheduling kernel, Form. Methods Syst. Des., 26 (2005) 103-135.

Digital Library

[15]

O. Tkachuk, M.B. Dwyer, C.S. Pasareanu, Automated environment generation for software model checking, in: 18th IEEE International Conference on Automated Software Engineering, IEEE Computer Society, 2003, pp. 116-129.

Digital Library

[16]

K. Yatake, T. Aoki, Automatic generation of model checking scripts based on environment modeling, in: Lecture Notes in Computer Science, vol. 6349, Springer, 2010, pp. 58-75.

[17]

J. Hatcliff, M.B. Dwyer, H. Zheng, Slicing software for model construction, High.-Order Symb. Comput., 13 (2000) 315-353.

[18]

M. Weiser, Program slicing, IEEE Trans. Softw. Eng., 10 (1984) 352-357.

Digital Library

[19]

OSEK/VDX portal, . http://portal.osek-vdx.org/

[20]

M. Acharya, B. Robinson, Practical change impact analysis based on static program slicing for industrial software systems, in: Proceedings of the 33rd International Conference on Software Engineering, ACM, 2011, pp. 746-755.

[21]

K.B. Gallagher, J.R. Lyle, Using program slicing in software maintenance, IEEE Trans. Softw. Eng., 17 (1991) 751-761.

Digital Library

[22]

M.P.E. Heimdahl, M.W. Whalen, Reduction and slicing of hierarchical state machines, in: Lecture Notes in Computer Science, vol. 1301, Springer, 1997, pp. 450-467.

[23]

R.M. Hierons, M. Harman, C. Fox, L. Ouarbya, M. Daoudi, Conditioned slicing supports partition testing, Softw. Test. Verif. Reliab., 12 (2002) 23-28.

[24]

J. Béchennec, M. Briday, S. Faucou, Y. Trinquet, Trampoline: an open source implementation of the OSEK/VDX RTOS specification, in: Proceedings of 11th IEEE International Conference on Emerging Technologies and Factory Automation, IEEE, 2006, pp. 62-69.

[25]

E.M. Clarke, D. Kroening, F. Lerda, A tool for checking ANSI-C programs, in: Lecture Notes in Computer Science, vol. 2988, Springer, 2004, pp. 168-176.

[26]

AUTomotive Open Source ARchitecture. http://www.autosar.org/

[27]

ISO CD 26262: Road vehicles - functional safety, part 1-9, 2008.2.29.

[28]

F. Tip, A survey of program slicing techniques, Center for Mathematics and Computer Science, Amsterdam, 1994.

[29]

MISRA home, . http://misra.org.uk/

[30]

Y. Choi, Constraint specification and test generation for OSEK/VDX-based operating systems, in: Lecture Notes in Computer Science, vol. 8137, Springer, 2013, pp. 305-319.

[31]

Eclipse CDT, . http://www.eclipse.org/cdt/

[32]

. http://www.froglogic.com/squish/coco/

[33]

D. Binkley, The application of program slicing to regression testing, Inf. Softw. Technol., 40 (1998) 583-594.

[34]

R. Gupta, M.J. Harrold, M.L. Soffa, An approach to regression testing using slicing, in: Proceedings of the Conference on Software Maintenance, IEEE, 1992, pp. 299-308.

[35]

O. Chebaro, N. Kosmatov, A. Giorgetti, J. Julliand, Program slicing enhances a verification technique combining static and dynamic analysis, in: Proceedings of the ACM Symposium on Applied Computing, ACM, 2012, pp. 1284-1291.

[36]

N. He, M.S. Hsiao, Bounded model checking of embedded software in wireless cognitive radio systems, in: 25th International Conference on Computer Design, IEEE, 2007, pp. 19-24.

[37]

A. Gupta, K.L. McMillan, Z. Fu, Automated assumption generation for compositional verification, Form. Methods Syst. Des., 32 (2008) 285-301.

Digital Library

[38]

W. Nam, P. Madhusudan, R. Alur, Automatic symbolic compositional verification by learning assumptions, Form. Methods Syst. Des., 32 (2008) 207-234.

Digital Library

[39]

P. Parizek, F. Plasil, Partial verification of software components: heuristics for environment construction, in: 33rd EUROMICRO Conference on Software Engineering and Advanced Applications, IEEE Computer Society, 2007, pp. 75-82.

[40]

M.B. Dwyer, C.S. Pasareanu, Filter-based model checking of partial systems, in: 6th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ACM, 1998, pp. 189-202.

Digital Library

[41]

J. Chen, T. Aoki, Conformance testing for OSEK/VDX operating system using model checking, in: 18th Asia Pacific Software Engineering Conference, IEEE, 2011, pp. 274-281.

Digital Library

[42]

J. Shi, J. He, H. Zhu, H. Fang, Y. Huang, X. Zhang, ORIENTAIS: formal verified OSEK/VDX real-time operating system, in: 17th IEEE International Conference on Engineering of Complex Computer, IEEE Computer Society, 2012, pp. 293-301.

[43]

Y. Huang, Y. Zhao, L. Zhu, Q. Li, H. Zhu, J. Shi, Modeling and verifying the code-level OSEK/VDX operating system with CSP, in: 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, IEEE Computer Society, 2011, pp. 142-149.

[44]

N.S. Chowdhury, Y. Choi, Safety properties based scenario generation for model checking Trampoline OS, Int. J. Secur. Appl., 7 (2013) 121-132.

Cited By

Park MJang HByun TChoi YRothermel GBae D(2020)Property-based testing for LG home appliances using accelerated software-in-the-loop simulationProceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice10.1145/3377813.3381346(120-129)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377813.3381346
Zhang XLu FCui MFujita MDong JArai M(2019)A review of OSEK/VDX application verification methodsProceedings of the 5th International Conference on Communication and Information Processing10.1145/3369985.3370003(37-42)Online publication date: 15-Nov-2019
https://dl.acm.org/doi/10.1145/3369985.3370003
Ferles KWüstholz VChristakis MDillig IBodden ESchäfer WDeursen AZisman A(2017)Failure-directed program trimmingProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106249(174-185)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106249

Efficient safety checking for automotive operating systems using property-based slicing and constraint-based environment generation

Recommendations

Slicing-based Reductions for Rebeca

Slicing is a program analysis technique which can be used for reducing the size of the model and avoid state explosion in model checking. In this work a static slicing technique is proposed for reducing Rebeca models with respect to a property. For ...
Efficient Model Checking of PSL Safety Properties
ACSD '10: Proceedings of the 2010 10th International Conference on Application of Concurrency to System Design

Safety properties are an important class of properties as in the industrial use of model checking a large majority of the properties to be checked are safety properties. This work presents an efficient approach to model check safety properties expressed ...
Model Checking Safety-Critical Systems Using Safecharts

With rapid developments in science and technology, we now see the ubiquitous use of different types of safety-critical systems in our daily lives such as in avionics, consumer electronics, and medical systems. In such systems, unintentional design ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Science of Computer Programming

Science of Computer Programming Volume 103, Issue C

June 2015

112 pages

ISSN:0167-6423

Issue’s Table of Contents

Copyright © Elsevier B.V.

Publisher

Elsevier North-Holland, Inc.

United States

Publication History

Published: 01 June 2015

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Park MJang HByun TChoi YRothermel GBae D(2020)Property-based testing for LG home appliances using accelerated software-in-the-loop simulationProceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice10.1145/3377813.3381346(120-129)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377813.3381346
Zhang XLu FCui MFujita MDong JArai M(2019)A review of OSEK/VDX application verification methodsProceedings of the 5th International Conference on Communication and Information Processing10.1145/3369985.3370003(37-42)Online publication date: 15-Nov-2019
https://dl.acm.org/doi/10.1145/3369985.3370003
Ferles KWüstholz VChristakis MDillig IBodden ESchäfer WDeursen AZisman A(2017)Failure-directed program trimmingProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106249(174-185)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106249

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents