摘要
模型检测作为一种形式化验证技术已成功应用于硬件以及协议的性质验证过程,目前正转向软件验证领域并逐渐扩展其应用范围。针对特定的森林防火专家系统的知识库规则,研究其所需满足的性质规范的形式化验证问题。首先将规则体描述为状态迁移图,通过引入转换函数对状态迁移图的变迁过程及状态性质进行了有效说明,然后将性质规范描述为相应的时序逻辑表达式,最后通过实例对模型检测过程进行了详细说明,本文的研究成果有效地说明了将模型检测应用于森林防火专家系统等林业信息系统的可行性与正确性。
As a formal verification technique,model checking has been successfully applied in the property verification process of hardware and protocol,which is turning to the field of software verification and gradually expands its scope of application. Aiming to the knowledge base of expert system for forest fire prevention rules,the paper researches the formal verification problems for properties specification to be satisfied. Fist,the rule body is described as state transition graph and the state transition process and state properties of graphs are effectively illustrated by introducing the transfer function. Then the corresponding temporal logic expression for the properties specification is described. Finally,the model checking process is detailed described. The research results of this paper illustrate the feasibility and the correctness and prove that model checking can be applied to the forest fire prevention expert system and other forest information systems in a certain extent.
出处
《智能计算机与应用》
2014年第2期117-118,F0003,共3页
Intelligent Computer and Applications
基金
全国大学生创新创业训练计划项目(201310225064)
关键词
模型检测
知识库模型
状态迁移图
时序逻辑
Model Checking
Knowledge Base Model
State Transition Graph
Temporal Logic
