Petri 网是系统建模的形式化方法,为了解决其在软件需求建模和建立程序语义映射方面存在的不足,提出了一种扩展Petri网的方法来支持软件需求建模,区分了状态型和数值型库所,根据软件特点有针对性地扩展了变迁的可触发条件和迁移运算,同时建立了和模型检验程序语言的映射,将扩展Petri网作为检验的模型输入,利用时态逻辑描述运行性质,进行需求模型检验.定时器和航空发动机的防喘功能验证实例结果表明,扩展Petri网可以较好地支持软件系统需求建模和软件程序语义映射,通过模型检验和反例路径分析,可以达到修改和完善需求模型的目的,从而提高软件的质量和安全性.%Petri Net is a formal method of system modeling. To solve its insufficiencies in software requirement modeling and program semantic mapping, an extended Petri net was proposed to support the software requirement modeling. The state place and numerical value place were distinguished. The triggering condition of transition and the migration operation were pertinently expanded according to the characteristics of the software, and the semantic mapping of model checking program was built. The extended Petri net was regarded as the model input of checking, and the requirement model was checked through describing the operating character with the temporal logic. The verifying results in the timer and the anti-surge function of aero-engine show that the expanded Petri net can preferably support the software system requirement modeling and software programme semantic mapping. The modification and perfection of requirement model can be attained with the model checking and counterexample analysis, which is beneficial to the improvement in both quality and safety of the software.
展开▼
