摘要
为了解决研发流程设计与需求的不一致性问题,提出了一种基于任务单元模型和线性时序逻辑的研发流程验证方法。方法应用任务单元模型分解研发流程,采用Promela语言描述模型,线性时序逻辑表示抽象的研发过程规则,通过模型检测器Spin完成验证工作,从而实现了对流程正确性的判断。
To resolve the inconsistency between research and development process design and requirements,a novel method is proposed,which is based on task unit model and linear temporal logic.In this method,task unit model is employed to resolve research and development process,promela is used to describe the model,linear temporal logic is designed to give the abstract description of the research and development process rule,spin model checker presents the verification results,then it can determine the correctness of the process.
出处
《航空计算技术》
2013年第3期89-91,95,共4页
Aeronautical Computing Technique
基金
国家自然科学基金项目资助(61172147)
关键词
研发流程
任务单元模型
模型检测
线性时序逻辑
research and development process
task unit model
model checking
linear temporal logic
