[2015-1-8]不可行路径片段制导的线性混成自动机有界可达性检验及全局性质推导

文章来源:  |  发布时间:2014-12-29  |  【打印】 【关闭

  

Title: 不可行路径片段制导的线性混成自动机有界可达性检验及全局性质推导

       Hybrid Automata: On Bounded Reachability Checking Guided by Analysis of Infeasible Path Segments, and on Derivation of Global Properties

Speaker: 卜磊(南京大学)

         Lei Bu (Nanjing University, China)

         ( cs.nju.edu.cn/bulei )

Time: 8th January 2015, 09:30

Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS

Abstract:

混成自动机行为中离散跳转与连续实时行为相交织,其状态空间非常复杂难以验证。即使是面向相对简单的子类-线性混成自动机-相关问题业已被证明为不可判定。近年来相关工作主要在有界可达性验证层面展开。传统方法是将自动机在一定阈值内所有可能行为编码成一组SMT约束,并调用SMT求解器进行求解。然而,随着阈值数值的增大,对应SMT约束集的规模将快速增长从而限制了可验证问题的规模。

应对此问题,本课题组提出了离散与连续分层考虑的新型有界可达性验证算法。通过在离散层面寻找潜在路径,在连续层面确认的形式控制单次验证问题的规模。在此基础上当连续层面发现相关路径不可行时,定位其中不可行子路径片段并将其反馈至离散层面对待验证空间进行剪枝,从而高效完成相关验证。更进一步,当相关不可行子路径片段积累较多的时候,可以经常发现程序离散图结构上已经不存在能连通起点至目标点的潜在路径,在此情况下有界不可达性质可进一步被推广到全局状态空间。

Biography:

卜磊,现任南京大学计算机科学与技术系副教授,于2010年4月毕业于南京大学计算机科学与技术系,获博士学位。主要研究领域是软件工程与形式化方法,侧重于模型检验技术,实时和混成系统,信息物理融合系统等方向。曾在美国CMU、UTD、欧盟FBK、日本NII、微软亚洲研究院等科研机构进行访学与合作研究。目前已在相关领域内重要期刊与会议如 RTSS、TPDS、CAV、FMSD、STTT、FMCAD、DATE、VMCAI、ICCPS 等上发表论文三十余篇。