基于任务单元模型的研发流程验证  

Verification of Research and Development Process Based on Task Unit Model

作　　者：丁明[1] 张军[1] 朱沧[1] 张昕[1] 

机构地区：[1]中航工业西安航空计算技术研究所,陕西西安710119

出　　处：《航空计算技术》2013年第3期89-91,95,共4页Aeronautical Computing Technique

基　　金：国家自然科学基金项目资助(61172147)

摘　　要：为了解决研发流程设计与需求的不一致性问题,提出了一种基于任务单元模型和线性时序逻辑的研发流程验证方法。方法应用任务单元模型分解研发流程,采用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.

关 键 词：研发流程 任务单元模型 模型检测 线性时序逻辑 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]