基于层次组合抽象的智能系统形式化验证

作者：周益龙; 韩斌

来源：计算机与数字工程, 2019, (08): 1917-1920+1984.

• 形式化方法
• 智能系统
• 组合抽象模型
• 模型检测 formal method
• smart system
• combination abstract model
• model checking

论文针对智能系统提出了一种形式化建模和验证的方法:首先,采用层次化的思想将智能系统分为应用层、系统层和设备层,综合系统功能需求和硬件模块分别建立各层的Kripke结构模型;然后,根据组合模型规则将层次模型进行组合,经过抽象处理后得到系统组合抽象模型。最后,以能源共享系统为例,用CSP#描述系统模型、LTL描述系统性质,利用PAT工具完成系统模型的自动验证。实验结果表明,该方法综合考虑了系统各个主体的行为,能够有效找出智能系统中的设计缺陷,并且可以缓解模型检测中的状态空间爆炸问题。

• 单位
  江苏科技大学