Constraint specification and test generation for OSEK/VDX-based operating systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

12 Scopus citations

Abstract

This work suggests a method for systematically constructing an environment model for automotive operating systems compliant with the OSEK/VDX international standard by introducing a constraint specification language, OSEK-CSL, and defining its underlying formal models. OSEK-CSL is designed for specifying constraints of OSEK/VDX using a pre-defined set of constraint types identified from the OSEK/VDX standard. Each constraint specified in OSEK-CSL is interpreted as a context-free language and is converted into push-down automata using NuSMV, which allows automated test sequence generation using LTL model checking. This approach supports selective applications of constraints and thus is able to control the "degree" of test sequences with respect to test purposes. An application of the suggested approach demonstrates its effectiveness in identifying safety problems.

Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods - 11th International Conference, SEFM 2013, Proceedings
Pages305-319
Number of pages15
DOIs
StatePublished - 2013
Event11th International Conference on Software Engineering and Formal Methods, SEFM 2013 - Madrid, Spain
Duration: 25 Sep 201327 Sep 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8137 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th International Conference on Software Engineering and Formal Methods, SEFM 2013
Country/TerritorySpain
CityMadrid
Period25/09/1327/09/13

Fingerprint

Dive into the research topics of 'Constraint specification and test generation for OSEK/VDX-based operating systems'. Together they form a unique fingerprint.

Cite this