Constraint-based test generation for automotive operating systems

详细信息    查看全文

• 作者：Yunja Choi ; Taejoon Byun
• 关键词：Verification ; Constraint specification ; Operating system ; Automotive software ; Test generation
• 刊名：Software & Systems Modeling
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：16
• 期：1
• 页码：7-24
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Software Engineering/Programming and Operating Systems; Programming Techniques; Software Engineering; Programming Languages, Compilers, Interpreters; Information Systems Applications (incl.Internet);
• 出版者：Springer Berlin Heidelberg
• ISSN：1619-1374
• 卷排序：16

文摘

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.