加入收藏夹
联系我们
关于本站
个人主页
西电导航
西安电子科技大学
    当前位置:首页>>学术讲座
Linear Temporal Logic and Model Checking
时间:2017-06-22 17:26    点击:   所属单位:机电工程学院
讲座名称 Linear Temporal Logic and Model Checking
讲座时间 2017-06-30 08:30:00
讲座地点 北校区主楼III-143北
讲座人 Lei Feng
讲座人介绍 Lei Feng is an associate professor at the Mechatronics and Embedded Control Systems division, KTH Royal Institute of Technology, Stockholm, Sweden. His main research interests include formal methods for the verification and control synthesis of cyber-physical systems, energy management control of mechatronic systems, and supervisory control of discrete-event systems. He
received the B.S. and M.S. degrees from the Department of Mechanical and Electronic Engineering, Xi’an Jiaotong University, Xi’an, China, in 1998 and 2001, respectively, and the Ph.D. degree with the Systems Control Group, Department ofElectrical and Computer Engineering, University of Toronto, Toronto, ON, Canada, in 2007. He was a research engineer at Volvo Technologies Corporation, Sweden, from 2009 to 2012, and joinedKTH as an assistant professor in 2012.
讲座内容 The course contains two parts. The first part is on the introduction of linear temporal logic (LTL) and the second part on LTL model checking. LTL is a major branch of temporal logic and effective for specifying logical and sequential constraints of software execution. It is widely applied in software engineering, requirement management, and formal methods for verification and testing. Model checking is a prominent formal verification technique for assessing functional properties of computer and software-intensive systems. It requires a model of the system under consideration and a formal specification of the requirement. The formal specification is often an LTL formula. A model checker is a software program that can automatically and exhaustively check if the given design model satisfies thespecification. The checking result either asserts the correctness of the design model or provides a counterexample in the design model that violates the specification. Compared to simulation and testing, model checking can efficiently enumerate all reachable states to reach 100% coverage in the design model.
课程安排:
  课程内容 时间 地点
1 Fundamental definitions of finite state automata and LTL 6月30日星期五
上午 8:30--10:30
 
 
 
 
 
北校区主楼III-143北
2 LTL properties and semantics
 
7月3日星期一
上午 8:30--10:30
3 Specifications using LTL 7月5日星期三
上午 10:15—12:15
4 Brief Introduction to the model checker SPIN 7月7日星期五
上午 8:30--10:30
5 Basic syntax and semantics of SPIN 7月10日星期一
上午 8:30--10:30
6 LTL model checking with SPIN
 
7月12日星期三
上午 10:15—12:15


转载请注明出处:西安电子科技大学学术信息网
如果您有学术信息或学术动态,欢迎投稿。我们将在第一时间确认并收录,投稿邮箱: meeting@xidian.edu.cn
Copyright © 2011-2017 西安电子科技大学 
开发维护:电子工程学院网络信息中心  管理员:meeting@xidian.edu.cn 站长统计: