航空计算技术
航空計算技術
항공계산기술
AERONAUTICAL COMPUTER TECHNIQUE
2013年
3期
89-91,95
,共4页
研发流程%任务单元模型%模型检测%线性时序逻辑
研髮流程%任務單元模型%模型檢測%線性時序邏輯
연발류정%임무단원모형%모형검측%선성시서라집
research and development process%task unit model%model checking%linear temporal logic
为了解决研发流程设计与需求的不一致性问题,提出了一种基于任务单元模型和线性时序逻辑的研发流程验证方法.方法应用任务单元模型分解研发流程,采用Promela语言描述模型,线性时序逻辑表示抽象的研发过程规则,通过模型检测器Spin完成验证工作,从而实现了对流程正确性的判断.
為瞭解決研髮流程設計與需求的不一緻性問題,提齣瞭一種基于任務單元模型和線性時序邏輯的研髮流程驗證方法.方法應用任務單元模型分解研髮流程,採用Promela語言描述模型,線性時序邏輯錶示抽象的研髮過程規則,通過模型檢測器Spin完成驗證工作,從而實現瞭對流程正確性的判斷.
위료해결연발류정설계여수구적불일치성문제,제출료일충기우임무단원모형화선성시서라집적연발류정험증방법.방법응용임무단원모형분해연발류정,채용Promela어언묘술모형,선성시서라집표시추상적연발과정규칙,통과모형검측기Spin완성험증공작,종이실현료대류정정학성적판단.
