望安科技自主研发的验证工具PiCore在第四届全国形式化方法与应用会议上亮相

近日，望安科技董事长、北京航空航天大学赵永望教授应邀参加第四届全国形式化方法与应用会议，并做相关学术报告。在会上，赵永望教授对望安科技自主研发的并发反应式系统组合验证工具PiCore做了全面介绍。

第四届全国形式化方法与应用会议（FMAC 2019）于 2019 年 11 月 30 日至 12 月 1 日在上海举行。形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已延生成为计算思维的重要载体。第四届全国形式化方法与应用会议(FMAC 2019)由中国计算机学会主办，形式化方法专业委员会联合承办。会议汇聚了来自新加坡国立大学、香港科技大学、清华大学、北京大学、中国科学院、南京大学、北京航空航天大学、国防科技大学等国内外顶级高校和航空航天、轨道交通等工业界的200多位专家学者。

望安科技董事长、北京航空航天大学赵永望教授，应邀在FMAC青年学者论坛做“并发反应式系统组合验证方法、实现及应用”的学术报告，全面介绍公司的并发系统验证工具PiCore。

系统多核化、网络化、服务化的发展趋势下，现代高保障(High-assurance)系统大多是并发反应式系统，例如操作系统(OS)、控制系统、业务流程系统等，这类系统的形式化验证仍然面临很多的挑战。本公司针对市场需求，研发了一个并发反应式系统组合验证工具PiCore，采用Rely-Guarantee理论和事件驱动的方式，支持抢占、中断、资源锁等并发机制的模型化和组合验证。PiCore采用“适配器”的设计模式，实现了多种形式化语言的“零修改”集成，目前已集成了一系列第三方的形式化验证语言。该工具已成功应用到Linux基金会Zephyr RTOS的形式化验证、业务流程语言BPEL的形式化验证等。