中文摘要：

混成系统的模型检验技术对实时系统质量保障具有重要意义。由于系统行为高度复杂，现有工作主要针对线性混成自动机的可达性检验，但可解决问题规模过小不足以满足实际应用需要。同时，现有技术在非线性混成自动机可达性检验及混成自动机活性检验两个重要应用领域所展开的工作颇为有限，亟待进一步研究。近年来，CPS系统广泛兴起，混成自动机作为其自然的建模语言，其模型检验问题显得愈发重要。与一般嵌入式系统不同，CPS系统行为具有高度不确定性，因此传统的离线建模验证技术已无法满足CPS系统的需要，如何应对此需求对CPS系统进行验证也是一个重要科学问题。本课题将基于已有工作展开，以面向路径可达性检验为基础，数值约束技术为手段，多核技术为平台，服务于应用为目标，设计面向（非）线性混成自动机可达性，线性混成自动机活性的验证算法，以此为基础设计支持CPS系统的在线建模验证框架，并结合典型CPS安全攸关系统进行示范性应用。

结论摘要：

随着实时、嵌入式系统乃至信息物理融合系统愈发广泛地出现在人们生产生活的方方面面，如何保证相关系统的正确性，保证系统应用过程中不会出现危险是一项迫在眉睫的需求。在基金委的资助下，本项目从理论层混成自动机的多种性质模型检验技术、应用层信息物理融合系统的在线验证技术以及信息物理融合系统底层无线传感网络的验证、设计等技术进行了系统研究。提出了包括多技术深度融合的有界模型检验技术、基于不可行子路径定位的有界结果全局拓展、基于等价迁移系统构造的混成系统活性、稳定性验证、信息物理融合系统在线建模验证等系列技术。相关技术在包括列控、医疗手术系统在内的信息物理融合系统仿真平台上进行实例研究，充分证明了其有效性。 项目实施3年来，发表录用了高质量论文15篇，其中包括CCF－A论文三篇 （包括两篇IEEE Transactions on Parallel and Distributed Systems, 一篇RTSS2014），CCF－B论文两篇（包括DSN2013与Formal Methods in System Design），一级学报《中国科学》、《软件学报》等。此外，在CPS系统领域旗舰会议ICCPS上连续多年发表了包括Regular、Poster、Demo、WIP在内的系列文章。同时项目组还出版译著一部。 本项目申请国家发明专利8项，获取软件著作权6项。本课题开发了面向混成自动机有界模型检验工具BACH系列，面向CPS系统在线建模与验证BACH Online系列， 基于迁移系统的混成自动机活性、稳定性分析工具HVT系列等多项工具。相关工具在线免费发布，引起广泛关注，下载次数过百，其中不乏美国卡耐基梅陇，加州大学伯克利分校等顶级学府的研究人员。本工作所取得成果取得广泛影响， 相关工作在国内外受邀报告多次，包含美国卡耐基梅隆大学、日本国立情报学研究所、新加坡工业设计大学、中国科学院软件所、江苏省计算机协会年会等。 特别值得一提的是本工作所提出的混成自动机有界模型检验及在线建模验证工作在国际一流会议FM2014上进行了半天的专题Tutorial报告，这也充分证明了本工作的被认可程度。