“青年学者论坛”学术报告(卜磊)

“青年学者论坛”学术报告（8）

报告人： 卜磊 博士
时  间： 2010年10月29日 (星期五)  10:00-11:20
地  点： 蒙民伟楼109

混成系统面向路径有界可达性研究

摘要： 混成系统是一类有广泛应用的基于计算机的系统，例如嵌入式系统、CPS系统等均可认为是混成系统的典型示例。当前混成自动机是其主要设计建模语言，对混成自动机进行可达性检验是提高系统设计质量的重要途径。目前混成自动机的可达性检验均直接面向系统完整状态空间或者阈值内所有状态空间，在可检验系统的规模上受到很大的限制，离工业界的实际应用需求尚有相当大的距离。为了满足工业界的实际应用需求，增大可检验系统的规模，本报告从一个新的角度对混成系统可达性检验问题展开研究：
1.从有界模型检验的角度出发将线性混成自动机的有界可达性问题分解成各路径的可达性问题来降低问题规模并控制问题的复杂度，在此基础上结合路径遍历技术完成阈值内全状态空间的检验。
2.针对组合系统，通过针对路径集中共享事件位置添加同步约束从而规避笛卡尔乘积，精简目标约束集规模，增大可检验组合系统的规模。
3.将所提出的面向路径有界可达性检验途径扩展至非线性混成自动机，在非线性混成自动机一个子类—凸性自动机上建立了相关面向路径的有界可达性检验技术。

简介：卜磊，南京大学计算机科学与技术系讲师。主要研究领域是软件工程与形式化方法，包括模型检验技术，实时混成系统，CPS系统，嵌入式系统以及软件建模、测试与验证等多个方向。2010年于南京大学获取计算机博士学位，攻博期间曾在美国Carnegie Mellon University (CMU)、美国University of Texas at Dallas (UTD)、欧盟Fondazione Bruno Kessler（FBK-IRST）等科研机构进行访学与合作研究。已在相关领域内重要期刊与会议如STTT，FMCAD，DATE，VMCAI等上发表论文十余篇。