[02-25] Towards Verified and Certifiable Subsystems

文章来源:  |  发布时间:2019-02-21  |  【打印】 【关闭

  

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

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