应王恪铭博士的邀请，英国南安普顿大学高级研究员Dr. Colin Snook访问了实验室。Colin博士是B方法专家，主要从事UML-B及RODIN平台的开发，Colin博士在过去20年中一直致力于与航空航天和铁路领域的企业进行合作的研究项目。
在访问期间的11月18日下午，Colin博士以目前进行的欧盟Enable-S3研究项目，报告了对欧洲铁路系统的验证工作，题名为《Behavior Driven Formal Model Development of the ETCS Hybrid Level 3》,实验室陈树伟副教授主持了报告。
在报告中，Colin博士首先介绍了Event-B语言的RODIN开发平台以及UML开发工具，举例讲述了如何对失败的证明义务进行人机交互式的验证；接下来，以欧洲列车控制系统(ETCS)—混成Level 3级系统为例，介绍了基于行为驱动的形式化建模过程，及应用到实际规范中的研究经验。
报告持续了近两个小时，在报告过程之中及Colin博士讲述结束后，实验室师生踊跃提问交流，对精化、验证、场景测试等问题进行了进一步的交流。通过此次学术报告，拓宽了实验室师生对Event-B方法的认识，增强了对形式化验证过程的理解，促进了大家今后的研究工作。
19日上午，Colin博士与实验室形式化验证研究组进行了针对铁路控制系统验证的研讨，王恪铭博士主持。铁路控制系统是具有安全苛求特性的离散系统，此类系统的形式化建模与验证一直是行业的难点与热点问题。
首先，研究组师生分别简要介绍了各自的研究工作。之后，分别就目前在工业应用方面所遇到的问题提出来与Colin博士进行讨论，如Atelier B平台外接一个新的UML-B的插件，外接证明器，如何正确地构建一个庞大复杂的B模型以及具体案例的验证问题等相关系列问题。Colin博士结合经验，给出了自己的理解和解决方案建议，并借助黑板和大家进行了深入的讨论，研讨一直持续到12点之后结束。
在Colin博士访问期间，研究组成员们也多次与Colin博士进行了小范围的讨论，基于铁路行业实际形式化验证项目的案例，研究讨论了可行的解决方案。此次系列活动进一步加深了研究组成员对B方法建模研究的认识，增加了应对工业验证之中困难与挑战的信心。
(供稿：程鹏, 王恪铭, 2019-11-22)
