英国 南安普顿大学 Dr Colin Snook 学术报告:Behavior Driven Formal Model Development of the ETCS Hybrid Level 3

来源:信息科学与技术学院  作者:王恪铭  日期:2019-11-14  点击数:292

报告题目(Title):  Behavior Driven Formal Model Development of the ETCS Hybrid Level 3

报告专家(Speaker):  Dr Colin Snook, Senior Research Fellow, University of Southampton, UK

报告地点(Venue):  西南交通大学九里校区0号楼10楼 01020#会议室

报告时间(Time):  2019-11-18 周一 15:00-17:00

主持人(Chair):  王恪铭(Keming Wang)

内容提要(Outline of the talk):

In this talk Dr Colin Snook will give an overview of the formal methods and tools that they use at University of Southampton, focusing particularly on those that they have developed during the Enable-S3 project. He will give an overview of the formal models of some railway case studies and their experiences of verifying their safety using the Event-B theorem provers and model checker. However, although safety is important, they also need the models to be useful and to reflect the desired behaviour of the system. They have therefore focused more recently on techniques to test the behaviour of their models in a systematic way using scenarios. He will discuss lessons learned from applying this behaviour driven formal modelling process to a real-life specification: The European Train Control Systems (ETCS) Hybrid Level 3.


报告人简介(Short Biography of the speaker)

Dr Colin Snook is a Senior Research Fellow at University of Southampton, UK. Dr Snook is best known for developing UML-B which is a UML-like diagrammatic front-end for the Event-B formal modelling language. Dr Snook has spent the past 20 years working on collaborative research projects with Industry in the Aerospace and Railway domains. This has included constructing or consulting on formal modelling as well as developing formal modelling tools and training industry in their use. Most recently Dr Snook has been working on the Enable-S3 project developing formal modelling tools and techniques to support the verification of European railway systems.