首页  >  科学研究  >  学术动态

中科院软件所两位研究员来我院作学术报告

20161130日下午,中科院软件所李广元研究员和朱雪阳副研究员分别为我院师生做了题为《度量时序逻辑MTL{0,}的模型检测》和《同步数据流图的优化与调度研究》的学术报告。

李广元博士现为中国科学院软件研究所计算机科学国家重点实验室研究员,主要从事实时系统的形式化验证技术与验证工具的研究。他于2009年首次在国际上实现了时间自动机关于线性时序逻辑LTL的符号化模型检测工具,相关结果被国际同行作为“定理”、“命题”等在国际顶级刊物上加以引用,并被国外一些知名模型检测工具如UPPAALLTSmin以及DiVinE等用于时间自动机的活性性质和LTL性质的模型检测。此外他还与丹麦科学家合作实现了加权度量区间时序逻辑的统计模型检测以及度量区间时序逻辑的有效控制器合成。

朱雪阳博士现为中国科学院软件研究所计算机科学国家重点实验室副研究员。主要从事嵌入式系统设计、性能分析与优化及形式化方法等方面研究。作为技术骨干,先后参加了多项国家自然科学基金、863项目的研究工作;目前主持一项基金面上项目。在嵌入式系统设计及形式化方法领域的主流国际期刊(IEEE Trans. On CAD)、国际会议(RTAS, DATE, FM, ICFEM, ICECCS)及国内一级学报发表多篇论文。

本次讲座两位专家主要围绕同步数据流建模,模型分析,以及模型检测等方面技术进行了详细介绍。模型检测是一种基于状态空间搜索的形式化验证技术,是提高系统正确性的重要手段。而同步数据流作为一种特殊的数据流语言,具有良好的可分析特性,已在基于流处理的嵌入式系统的建模方面得到广泛应用。通过深入浅出的介绍,两位专家向大家介绍了这一领域的重要概念、问题、应用,以及展示了中科院软件所在这一领域近期的研究进展。在讲座最后,师生们就这一领域的问题和前景与两位专家进行了问答和热烈的讨论。

〖来自于〗 〖发布日期〗2016-12-05