2021年4月15日，由王恪铭老师讲授的西南交通大学创新讲座之形式化方法及其在安全苛求系统开发中的应用在西南交通大学犀浦校区X2423教室顺利举行。王恪铭老师主要向同学们讲述了形式化方法，验证及其应用情况，从形式化方法和验证角度，结合研究团队的研究工作，对形式化应用的重要性做出了介绍。
王恪铭老师就“形式化验证简介”，“形式化验证应用概况”及“实验室研究方向”三个方面进行讲解。
当讲到形式化验证简介时，王老师先为同学们介绍了其产生背景—1996年欧洲阿丽亚娜5型导弹坠毁，由此分析了系统缺陷产生的本质原因：系统本身的复杂性或是技术上的复杂性。接着，王老师以需求阶段为例构造了系统开发过程的V模型，证明了“Bug发现越早，成本越低”。此后，王老师列举了众多减少Bug的手段，并引出了形式化方法及形式化验证的概念，形式化验证即基于形式化方法，对系统状态，动作行为等进行语义描述，并根据系统规范对系统的属性及正确性进行验证，以揭示系统设计中的错误。随后，王老师以源码的形式为例为同学们解释了形式化验证的方法原理与发展历程。在讲座的第二部分，王老师提到了形式化验证的应用。首先他以ABB计算机联锁系统为例介绍了应用的开发流程，紧接着讲到了形式化验证应用中的需求规范验证以及测试例生成，之后王老师以航天航空行业为例对形式化验证行业应用进行了概述，指出形式化验证方法的应用要求已经成安全苛求行业的标准。最后王老师粗略介绍了其实验室研究方向，并向同学们讲解了形式化方法研究的主要从事工作及其典型应用服务案例。
王恪铭老师与同学们进行了深入的沟通与思考，使同学们更加了解了形式化方法及其应用，激发了同学们浓厚兴趣。
