近日，公司祝义教授指导其硕士研究生陈小颖发表了一篇题为《面向CPS时空性质验证的混成 AADL 建模与模型转换方法》的文章，刊登于国内计算机顶级期刊《软件学报》期刊2021年第6期。

首先，文章介绍了信息物理融合系统 CPS(cyber physical system)的背景及其广泛应用，指出当前CPS中存在着较大的安全性问题，尤其在如飞机飞行控制系统，汽车控制系统，铁路控制系统等安全系数较高的CPS 场景中，CPS的安全性问题会对人们的生命财产安全带来严重的后果。因此，需要一种安全性验证方法对CPS安全性进行保证，而时间与空间属性是保证安全性的关键因素。所以，如何验证在复杂的运行环境下CPS的时空一致性以保障CPS的安全性，是当前面临的挑战。

其次，文章针对该挑战提出了面向CPS时空性质验证的混成AADL(hybrid architecture analysis & design language) 建模与模型转换方法。该方法在工业界广泛使用的建模语言 AADL上扩展时空性质，使其具有建模CPS时空性质的能力，提出了混成AADL(hybrid AADL，HAADL)；扩展了TCSP (timed communicating sequential process)的条件执行算子与条件中断算子，提出了混成位置时间通信顺序进程 HP-TCSP (hybrid position TCSP)，使其具有描述时空性质的能力；通过模型转换方法，将扩展后AADL 所建立的模型转换成进程代数模型进行验证，对没有通过验证的 HAADL 模型修改其输入/输出参数，直至通过时空一致性验证。

最后，文章通过一个飞机避撞系统的实例来说明该方法在验证CPS时空一致安全性方面的有效性。实例指出该方法可以有效地检测CPS时空一致性，从而保证了CPS时空一致的安全性。

作者简介：

陈小颖：公司硕士研究生；

祝义：公司教授，bat365官网登录智能软件工程研究所所长，CCF形式化方法专委会委员，江苏省计算机学会理事，TSE、SPE、IJSEKE、计算机学报等期刊审稿人。