Verifying Scheduling Point Constraints with Model Checking

摘要：

In this paper, we propose a method to verify whether a model is consistent to the scheduling point constraints in OSEK specification for non preemptive tasks. A simple operating system model is constructed and used to be the verification object. For verification, we build an auxiliary task set to interact with OS model, which makes the violation of scheduling point constraints appear. The property LTL formulae are generated from the constraints, which are verified by model checker SPIN. It is shown that our method can detect design mistakes.

关键词： verification model checking scheduling point OSEK/VDX

作者: Wei Sheng Gangyong Jia Li Xi Xuehai Zhou

作者单位: Department of Computer Science and Technology University of Science and Technology of China (USTC) H Department of Computer Science and Technology University of Science and Technology of China (USTC) H

会议类型: 国际会议

会议名称: 2011 International Conference on System Modeling and Optimization(ICSMO 2011)(2011年系统建模与优化国际会议)

会议地点: 贵阳

会议语种:英文

页码: 31-35

在线出版日期: 2011-01-26（万方平台首次上网日期，不代表论文的发表时间）