TY - GEN
T1 - Constraint specification and test generation for OSEK/VDX-based operating systems
AU - Choi, Yunja
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84885942258&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40561-7_21
DO - 10.1007/978-3-642-40561-7_21
M3 - Conference contribution
AN - SCOPUS:84885942258
SN - 9783642405600
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 305
EP - 319
BT - Software Engineering and Formal Methods - 11th International Conference, SEFM 2013, Proceedings
T2 - 11th International Conference on Software Engineering and Formal Methods, SEFM 2013
Y2 - 25 September 2013 through 27 September 2013
ER -