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

摘要

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