Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling
Erschienen in: Software and Systems Modeling 1/2017

06.01.2015 | Special Section Paper

Constraint-based test generation for automotive operating systems

verfasst von: Yunja Choi, Taejoon Byun

Erschienen in: Software and Systems Modeling | Ausgabe 1/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Vorheriger Artikel Introduction to the Software Engineering and Formal Methods 2013 special issue
Nächster Artikel Inferring physical units in formal models

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
We could not apply a C code model checker directly for system-level model checking since the code is dependent on the hardware platform, e.g., code for context switching.
 
2
A regular language can be formalized using a finite automaton which is a case of pushdown automaton.
 
Literatur
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)
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)CrossRefMATH
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)
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)
6.
EI-Fakih, K., Yevtushenko, N., von Bochmann, G.: FSM-based incremental conformance testing methods. IEEE transactions Softw. Eng. 30(7), 425–436 (2004)
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)CrossRef
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)
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)
12.
Uzuncaova, E., Khurshid, S., Batory, D.: Incremental test generation for software product lines. IEEE transactions on software engineering, pp. 309–322 (2010)
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)
14.
Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. Form. Methods Test. (2008)
15.
Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Form. Methods System Design (2009)
16.
17.
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.
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)
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)
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)
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)
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)
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)
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)
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)
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)CrossRefMATH
31.
de la Riva, C., Tuya, J.: Automatic generation of assumptions for modular verification of software specifications. J. Syst. Softw. (2006)
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)
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)
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)CrossRef
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)
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)
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)
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)
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)CrossRef
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)
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)
43.
de Moura, L., Jovanovi, D.: A model-constructing satisfiability calculus. In: 14th international conference on verification, model checking, and abstract interpretation (2013)
Metadaten
Titel
Constraint-based test generation for automotive operating systems
verfasst von
Yunja Choi
Taejoon Byun
Publikationsdatum
06.01.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 1/2017
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-014-0449-6

Weitere Artikel der Ausgabe 1/2017

Software and Systems Modeling 1/2017 Zur Ausgabe

Regular Paper

An empirical approach toward the resolution of conflicts in goal-oriented models

Editorial

Introduction to the theme issue on variability modeling of software-intensive systems

Theme Section Paper

The shape of feature code: an analysis of twenty C-preprocessor-based systems

Theme Section Paper

Variability testing in the wild: the Drupal case study

Theme Section Paper

Empirical assessment of two approaches for specifying software product line use case scenarios

Special Section Paper

Inferring physical units in formal models