时 间：2013年9月10日18:30 地 点：计算机楼229
主持人：王林章 副教授
报告一：混成系统协同控制的相关工作介绍
报告人：黄超
简介：混成系统是一类既包含连续动态行为又包含离散动态行为的系统,这类系统在实际应用中非常普遍。一些大规模的混成系统很多是由多个子混成系统联合构成的，这些子混成系统共享信息，并完成一个或多个共同的目标，例如列控系统，飞机编队等等。这类系统的协同控制策略如何设计是很重要的问题。目前，已经有一些工作是基于中央控制的协同控制。但是，中央控制需要有一个中央控制系统掌握并控制全局信息，受限于计算能力的制约，很难高效处理大规模的系统。我们希望能提出一种分布式的控制策略。分布式的控制策略可以将全局控制划分为多个局部控制问题，提高了大规模系统的控制效率。这种控制方法涉及到两个问题，混成系统的本地控制策略和对于协同关系的建模。本次报告根据以上两个问题，介绍了两位作者的工作。Claire J. Tomlin的工作是基于自动机技术的混成系统控制器综合。Tamas Keviczky的工作是基于模型预测控制技术的连续系统协同控制。
报告二：Inferring Invariants for Programs over Data Structures
报告人：翟娟
简介：程序验证是提高软件质量的重要手段之一。在分析验证时开发者给出了待验证程序的规范，但是对于基本语句，开发者一般不会给出规范。赋值语句和分支语句是有直接的转换规则。循环语句比较复杂，其中还可能嵌套了循环或者分支语句，通常是用循环不变式来描述循环初始时和执行过程中保持的性质，但是并不存在通用的规则来生成循环不变式，所以生成循环不变式是比较困难的。本报告提出了一种根据后置条件生成循环不变式的方法，这个方法用于处理依次遍历常用数据结构的循环体。首先，基于区间分割和模式匹配思想，根据后置条件猜测出候选的循环不变式，然后通过SMT来证明这些候选不变式的正确性。该方法已经实现并集成到Scope Logic工具中，实验结果表明我们提出的方法是有效的，生成的不变式可以较好地帮助证明程序的部分正确性。 |
