12月19日，应中国科学院深圳先进技术研究院数字所嵌入式软件系统研究室主任谷德权研究员的邀请，上海交通大学李国强博士赴深圳先进院作了题为“Modeling and Analysis of Real-Time Systems with Mutex Components”的学术讲座。

时间自动机(Timed Automata)是对实时系统进行形式化描述的有效手段。针对具有互斥组件(Mutex Components)的实时系统的描述问题，李博士提出了控制器自动机(Controller Automata)，通过聚焦组件之间的控制信息的传递来组合时间自动机。在控制器自动机中，每个状态被赋予一个时间自动机。在全局标记迁移中，状态中的时间自动机可能被控制信息抢占。由于使用了栈(Stack)，控制器自动机适当地扩展了表达能力，但也会导致可达性问题不可判定。李博士证明对具有严格偏序关系的状态集，不可判定的问题是可以避免的，并且控制器自动机可以翻译成时间自动机，对系统进行形式化分析。

本次讲座吸引了众多科研人员和学生的参与，现场气氛活跃。讲座之后，李博士分享了自己的科研经历，以及与Toyota、华为等公司的合作经验，并与科研人员和学生进行了广泛深入的交流。