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/