产品介绍：并发系统验证工具W-Concur

系统多核化、网络化、服务化的发展趋势下，现代高保障(High-assurance)系统大多是并发反应式系统，例如操作系统(OS)、控制系统、业务流程系统等，这类系统的形式化验证仍然面临很多的挑战。

本公司针对市场需求，研发了一个并发反应式系统组合验证工具W-Concur，采用Rely-Guarantee理论和事件驱动的方式，支持抢占、中断、资源锁等并发机制的模型化和组合验证。

并发系统验证工具：W-Concur

W-Concur是一款望安科技自主研制的并发系统形式化验证工具。该工具采用“适配器”的设计模式，实现了多种形式化语言的“零修改”集成。目前已集成了一系列第三方的形式化验证语言。该工具已成功应用到Linux基金会Zephyr RTOS的形式化验证、业务流程语言BPEL的形式化验证等。

该工具自主研发后，不断升级，并在许多实际场景中使用。