实验室刘静教授与瑞典专家在卡斯柯公司进行学术交流

       2015年1月26日至30日, 上海市高可信计算重点实验室刘静教授等四人在卡斯柯公司为联锁系统组进行形式化建模服务，与瑞典 Prover公司受邀来到卡斯柯信号有限公司的两位专家进行了深入讨论，分析轨道交通领域的形式化方法，以及Prover iLock形式化工具的应用。卡斯柯公司副总裁以及部门经理周庭梁高级工程师等二十余人参加交流。

       在研讨与交流的首日，周庭梁经理首先对实验室老师和Prover公司专家的到访表示欢迎，并简单介绍了卡斯柯公司的基本情况，特别是公司在形式化方法的研发方面。Prover公司专家对Prover iLock工具的主要的开发过程以及测试、验证方法进行了详细的介绍，并且进行了现场演示。

       之后几天中，实验室师生为卡斯柯公司进行了轨道联锁模型的建立、安全需求的描述、基于模型的测试、模型验证等工作探索，深入讨论期间遇到的问题，发现现有非形式化方法中存在的缺陷，并对此提出了解决方案。