Constraint Specification and Test Generation for OSEK/VDX-Based Operating Systems
Constraint Specification and Test Generation for OSEK/VDX-Based Operating Systems
复制标题
DOI：
10.1007/978-3-642-40561-7_21
复制
发表时间：
2013-09
影响因子：
7.4
通讯作者：
Yunja Choi
中科院分区：
文献类型：
--
作者：
Yunja Choi
通过引入约束描述语言OSEK_CSL并定义其底层形式化模型，提出了一种系统地构建符合OSEK/VDX国际标准的汽车操作系统环境模型的方法。OSEK_CSL设计用于使用OSEK/VDX标准中标识的一组预定义的约束类型来指定OSEK/VDX的约束。OSEK_CSL中指定的每个约束都被解释为上下文无关的语言，并使用NuSMV转换为下推自动机，这允许使用LTL模型检查自动生成测试序列。该方法支持约束的选择性应用，因此能够控制测试序列相对于测试目的的“程度”。该方法的应用表明，该方法在识别安全问题方面是有效的。
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.