一种面向CPS的控制应用程序协同验证方法

被引：7

作者：

张雨 ^{[1
,2
]}

董云卫 ^{[3
]}

冯文龙 ^{[1
,2
]}

黄梦醒 ^{[1
,2
]}

机构：

[1] 南海海洋资源利用国家重点实验室(海南大学)

[2] 海南大学信息科学技术学院

[3] 西北工业大学计算机学院

来源：

软件学报 | 2017年 / 28卷 / 05期

基金：

海南省自然科学基金;

关键词：

信息-物理融合系统; 嵌入式控制应用程序; 自动机理论; 协同验证; 有界模型检验;

D O I：

暂无

中图分类号：

TP311.1 [程序设计];

学科分类号：

081205 [计算机软件];

摘要：

信息-物理融合系统是一种新型嵌入式系统计算模式.它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息-物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性(safety)和活性(liveness)等属性要求,提出了对该模型进行形式化验证的算法:基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高了可验证系统的规模.另外,结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.

引用

页码：1144 / 1166

页数：23

共 4 条

[1]

信息物理融合系统控制软件的统计模型检验 [J].

单黎君 ;

周兴社 ;

王宇英 ;

赵雷 ;

万丽景 ;

乔磊 ;

陈建新 .

软件学报, 2015, 26 (02) :380-389

[2]

A Model-Based Toolchain to Verify Spatial Behavior of Cyber-Physical Systems [J].

Herrmann, Peter ;

Blech, Jan Olaf ;

Han, Fenglin ;

Schmidt, Heinz .

INTERNATIONAL JOURNAL OF WEB SERVICES RESEARCH, 2016, 13 (01) :40-52

[3]

Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study.[J].Kyungmin Bae;Joshua Krisiloff;José Meseguer;Peter Csaba Ölveczky.Science of Computer Programming.2014,

[4]

Model checking JAVA programs using JAVA PathFinder [J].

Havelund K. ;

Pressburger T. .

International Journal on Software Tools for Technology Transfer, 2000, 2 (4) :366-381

← 1 →