（通讯员：张佳峰）应yl9193永利官网系统控制与自动化实验室邀请，瑞典皇家理工学院的冯雷博士于2017年6月30日至7月12日，在yl9193永利官网开设了一门研究生课程“Linear Temporal Logic and Model Checking”。

该课程主要介绍线性时序逻辑（LTL）基础和基于Spin的模型检验方法。线性时序逻辑是时序逻辑的一个主要分支，用于形式化描述用户对于计算机软/硬件系统的各类需求，因此广泛应用于软件工程、需求管理工程等的系统形式化设计、验证与测试中。模型检验是针对用户需求对计算机软/硬件系统进行评估的一项技术。与传统的系统仿真与测试类技术相比，模型检验技术对于系统的考察更加完备，因此目前主要应用在安全关键系统的设计与开发中。

该课程为双语教学，共18学时。约20位研究生及青年教师全程参与了该课程。整个教学过程中既有严谨的数学推理，巧妙的算法思想，也有具体的实例演示，受到了选课同学的一致好评。冯雷博士也表示希望大家能在各自的科研工作中，考虑结合模型检验技术思想开展科研工作。

冯雷，博士、副教授，分别于1998年和2001年获得西安交通大学机械与电子工程学士与硕士学位，于2007年获加拿大多伦多大学电子与计算机工程博士学位，于2009年—2012年供职于瑞典沃尔沃技术公司，于2012年加入瑞典皇家理工学院机械电子与嵌入式控制系统系。他的研究兴趣主要有信息物理系统的形式化验证与控制综合，机电系统的能耗管理与控制，离散事件系统的监督控制。