Title: Towards Verified and Certifiable Subsystems 

　　Speaker: Prof.  Burkhart Wolff, University Paris-Sud 11 

　　Time: 15:00 pm, Feb. 25th (Monday), 2019 

　　Venue: Lecture room (Room 334), Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences 

　　Abstract: 本报告主要介绍Isabelle/HOL中开发的本体框架Isa_DOF，该框架提供一种支持强类型的本体定义语言，并通过Isabelle的IDE支持系统建模、验证与文档的平滑集成，从而解决系统安全认证过程中形式化模型/证据和非形式化文档之间的鸿沟。Isa_DOF框架支持系统文档的编写、确认和证据检查，并在Isabelle中与形式规范和形式证据进行良好的互动，通过不断地确认形式化和非形式化部分之间的一致性，解决大型系统安全认证中的关键问题。最后介绍本框架的一个应用案例：符合CENELEC规范的嵌入式铁路系统安全关键组件开发与验证。 

　　Biography: Burkhart Wolff是法国巴黎第十一大学(University Paris-Sud 11)的教授，VALS（算法、语言和系统验证）实验室的主任。主要从事形式化验证、系统安全认证、形式化测试等研究工作，参与了欧盟EUROMILS重大项目、法国Paral-ITP 项目、HOL-TestGen-XT项目等，研制了HOL-OCL模型驱动分析工具，HOL-Boogie、HOL-CSP等形式验证工具和HOL-TestGen等测试工具。 Wolff教授的团队目前正在开展PST项目研究，构建一个基于Isabelle/HOL的持续验证与认证环境(CVCE)工具链。Wolff教授目前的研究项目也包括编程和规范语言的语义表示，以及验证和测试技术在相关领域的应用。  homepage:  https://www.lri.fr/~wolff/