article

Constraint-based test generation for automotive operating systems

Authors:

Taejoon ByunAuthors Info & Claims

Software and Systems Modeling (SoSyM), Volume 16, Issue 1

Pages 7 - 24

https://doi.org/10.1007/s10270-014-0449-6

Published: 01 February 2017 Publication History

Abstract

This work suggests a method for systematically constructing a software-level environment model for safety checking automotive operating systems by introducing a constraint specification language, OSEK_CSL. OSEK_CSL is designed to specify the usage constraints of automotive operating systems using a pre-defined set of constraint types identified from the international standard OSEK/VDX. Each constraint specified in OSEK_CSL is interpreted as either a regular language or a context-free language that can be checked by a finite automaton or a pushdown automaton. The set of usage constraints is used to systematically classify the universal usage model of OSEK-/VDX-based operating systems and to generate test sequences with varying degrees of constraint satisfaction using LTL model checking. With pre-defined constraint patterns and the full support of automation, test engineers can choose the degree of constraint satisfaction and generate test cases using combinatorial intersections of selected constraints that cover all corner cases classified by constraints. A series of experiments on an open-source automotive operating system show that our approach finds safety issues more effectively than conventional specification-based testing, scenario-based testing, and conformance testing.

References

[1]

Choi, Y.: Constraint specification and test generation for OSEK/VDX-based operating systems. In: 11th International conference on software engineering and formal methods, lecture notes in computer science, vol. 8137, pp. 305---319. Springer, (2013)

Digital Library

[2]

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

[3]

Botaschanjan, J., Broy, M., Gruler, A., Harhurin, A., Kanpp, S., Kof, L., Paul, W., Spichkova, M.: On the correctness of upper layers of automotive systems. Form. Asp. Comput. 20, 637---662 (2008)

[4]

Lettnin, D., Nalla, P., Behrend, J., Ruf, J., Gerlach, J., Kropf, T., Rosenstiel, W., Schonknecht, V., Reitemeyer, S.: Semiformal verification of temporal properties in automotive hardware dependent software. In: Proceedings of design, automation, and test in Europe conference and exhibition (2009)

Digital Library

[5]

der Riden, T.I., Kanpp, S.: An approach to the pervasive formal specification and verification of an automotive system. In: Proceedings of the international workshop on formal methods in industrial critical systems (2005)

Digital Library

[6]

EI-Fakih, K., Yevtushenko, N., von Bochmann, G.: FSM-based incremental conformance testing methods. IEEE transactions Softw. Eng. 30(7), 425---436 (2004)

Digital Library

[7]

John, D.: OSEK/VDX conformance testing--MODISTARC. In: Proceedings of OSEK/VDX open systems in automotive networks (1998)

[8]

OSEK/VDX operating system specification 2.2.3

[9]

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

[10]

Gopinath, D., Zaeem, R.N., Khurshid, S.: Improving the effectiveness of spectra-based fault localization using specifications. In: 27th IEEE/ACM international conference on automated software engineering (2012)

Digital Library

[11]

Nebut, C., Fleurey, F., Traon, Y.L., Jézéquel, J.M.: Automatic test generation: a use case driven approach. IEEE Trans. Softw. Eng, pp. 140---155 (2006)

Digital Library

[12]

Uzuncaova, E., Khurshid, S., Batory, D.: Incremental test generation for software product lines. IEEE transactions on software engineering, pp. 309---322 (2010)

Digital Library

[13]

Weyuker, E.J., Goradia, T., Singh, A.: Automatically generating test data from a Boolean specification. IEEE transactions on software engineering, pp. 353---363 (1994)

Digital Library

[14]

Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. Form. Methods Test. (2008)

Digital Library

[15]

Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Form. Methods System Design (2009)

Digital Library

[16]

NuSMV: a new symbolic model checking. http://nusmv.irst.itc.it/

[17]

Trampoline--opensource RTOS project. http://trampoline.rts-software.org

[18]

Béchennec, J., Briday, M., Faucou, S., Trinquet, Y.: Trampoline: an opensource implementation of the OSEK/VDX RTOS specification. In: Proceedings of 11th IEEE international conference on emerging technologies and factory automation, pp. 62---69. IEEE (2006)

[19]

Park, M., Byun, T., Choi, Y.: Property-based code slicing for efficient verification of OSEK/VDX operating systems. First Int. Workshop Form. Tech. Saf. Crit. Syst. EPTCS 105, 69---84 (2012)

[20]

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

[21]

Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification, pp. 154---169 (2000)

Digital Library

[22]

Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th symposium on principles of programming languages, pp. 58---70. ACM (2002)

Digital Library

[23]

Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Proceedings of the 10th international conference on verification, model checking, and abstract interpretation. LNCS, vol. 5403, pp. 182---197 (2009)

Digital Library

[24]

Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interplant strength in model checking. In: Proceedings of the 24th international conference on computer aided verification, pp. 193---209 (2012)

Digital Library

[25]

Fraser, G., Gargantini, A.: An evaluation of model checkers for specification based test case generation. In: International conference on software testing verification and validataion (2009)

Digital Library

[26]

Zhou, L., Yao, M., Li, Y., Zhang, C., Yao, L.: A new specification-based test data generation strategy for OSEK OS. In: IEEE international conference on computer and information technology (2010)

Digital Library

[27]

Yatake, K., Aoki, T.: Automatic generation of model checking scripts based on environment modeling. In: 17th international SPIN conference on software model checking, lecture notes in computer science, vol. 6349, pp. 58---75. Springer (2010)

Digital Library

[28]

Fraser, G., Gargantini, A.: An evaluation of specification based test generation techniques using model checkers. In: Testing: academic and industrial conference--practice and research techniques, pp. 72---81 (2009)

Digital Library

[29]

Rayadurgam, S., Heimdahl, M.P.: Coverage based test-case generation using model checkers. In: Proceedings of the 8th annual IEEE international conference and workshop on the engineering of computer based systems, pp. 83---91 (2001)

[30]

Gupta, A., McMillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. Formal Methods in System Design 32(3), 285---301 (2008)

Digital Library

[31]

de la Riva, C., Tuya, J.: Automatic generation of assumptions for modular verification of software specifications. J. Syst. Softw. (2006)

Digital Library

[32]

Tkachuk, O., Dwyer, M.B., Pasareanu, C.S.: Automated environment generation for software model checking. In: 18th IEEE international conference on automated software engineering, pp. 116---129. IEEE Computer Society (2003)

Digital Library

[33]

Fang, L., Kitamura, T., Do, T.B.N., Ohsaki, H.: Formal model-based test for AUTOSAR multicore RTOS. In: Proceeding of the IEEE 5th international conference on software testing, verification and validation, pp. 251---259 (2012)

Digital Library

[34]

Carver, R.H., Tai, K.C.: Use of sequencing constraints for specification-based testing of concurrent programs. IEEE Tran. Softw. Eng. 24, 471---490 (1998)

Digital Library

[35]

de Alfaro, L., Henzinger, T.A.: Interface automata. In: 8th European software engineering conference/9th ACM/SIGSOFT international symposium on foundations of software engineering, pp. 109---120 (2001)

Digital Library

[36]

Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in reo by constraint automata. Sci. Comput. Programm. 61(2), 75---113 (2006)

Digital Library

[37]

Chen, J., Aoki, T.: Conformance testing for OSEK/VDX operating system using model checking. In: 18th Asia---Pacific software engineering conference, pp. 274---281. IEEE (2011)

Digital Library

[38]

Endres, E., Müller, C., Shadrin, A., Tverdyshev, S.: Towards the formal verification of a distributed real-time automotive system. In: Proceedings of NASA formal method symposium (2010)

[39]

Huang, Y., Zhao, Y., Zhu, L., Li, Q., Zhu, H., Shi, J.: Modeling and verifying the code-level OSEK/VDX operating system with CSP. In: 5th IEEE international symposium on theoretical aspects of software engineering, pp. 142---149. IEEE Computer Society (2011)

Digital Library

[40]

Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. Commun. ACM 53(6), 107---115 (2010)

Digital Library

[41]

Shi, J., He, J., Zhu, H., Fang, H., Huang, Y., Zhang, X.: ORIENTAIS: formal verified OSEK/VDX real-time operating system. In: 17th IEEE international conference on engineering of complex computer systems, pp. 293---301. IEEE Computer Society (2012)

Digital Library

[42]

Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: 18th international conference on computer-aided verification, pp. 81---94 (2006)

Digital Library

[43]

de Moura, L., Jovanovi, D.: A model-constructing satisfiability calculus. In: 14th international conference on verification, model checking, and abstract interpretation (2013)

Digital Library

Cited By

Brings JDaun M(2020)Towards automated safety analysis for architectures of dynamically forming networks of cyber-physical systemsProceedings of the IEEE/ACM 42nd International Conference on Software Engineering Workshops10.1145/3387940.3391474(258-265)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3387940.3391474
Kim DChoi YZimmermann TLawall JMarinov D(2019)Model checking embedded control software using OS-in-the-loop CEGARProceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2019.00059(565-576)Online publication date: 10-Nov-2019
https://dl.acm.org/doi/10.1109/ASE.2019.00059
Gurbuz HTekinerdogan B(2018)Model-based testing for software safetySoftware Quality Journal10.1007/s11219-017-9386-226:4(1327-1372)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1007/s11219-017-9386-2
Show More Cited By

Constraint-based test generation for automotive operating systems
1. Theory of computation

Recommendations

A Test Data Generation Approach for Automotive Software
QRS-C '15: Proceedings of the 2015 IEEE International Conference on Software Quality, Reliability and Security - Companion

Since automotive software contains many control flows, symbolic execution is an effective approach to generate test data for it. However, symbolic execution is cost expensive, so it is difficult to apply it directly. Moreover, parameters in automotive ...
Designing an Effective Constraint Solver in Coverage Directed Test Generation
ICESS '09: Proceedings of the 2009 International Conference on Embedded Software and Systems

As the complexity of processors grows, the bottleneck of verification remains in generating suitable test programs that meet coverage metrics automatically. Coverage directed test generation is a technique to automate the feedback from coverage analysis ...
Automated system-level safety testing using constraint patterns for automotive operating systems
SAC '15: Proceedings of the 30th Annual ACM Symposium on Applied Computing

The automotive operating system is a typical safety-critical system that is tightly coupled with the operational environment through system services. However, existing automated techniques come short of testing the interface of such operating systems. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Software and Systems Modeling (SoSyM)

Software and Systems Modeling (SoSyM) Volume 16, Issue 1

February 2017

298 pages

ISSN:1619-1366

Issue’s Table of Contents

Copyright © Copyright © 2017 Springer-Verlag Berlin Heidelberg.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 February 2017

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Brings JDaun M(2020)Towards automated safety analysis for architectures of dynamically forming networks of cyber-physical systemsProceedings of the IEEE/ACM 42nd International Conference on Software Engineering Workshops10.1145/3387940.3391474(258-265)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3387940.3391474
Kim DChoi YZimmermann TLawall JMarinov D(2019)Model checking embedded control software using OS-in-the-loop CEGARProceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2019.00059(565-576)Online publication date: 10-Nov-2019
https://dl.acm.org/doi/10.1109/ASE.2019.00059
Gurbuz HTekinerdogan B(2018)Model-based testing for software safetySoftware Quality Journal10.1007/s11219-017-9386-226:4(1327-1372)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1007/s11219-017-9386-2
Haghighatkhah ABanijamali APakanen OOivo MKuvaja P(2017)Automotive software engineeringJournal of Systems and Software10.1016/j.jss.2017.03.005128:C(25-55)Online publication date: 1-Jun-2017
https://dl.acm.org/doi/10.1016/j.jss.2017.03.005

View Options

View options

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