一种基于Event-B的多核并发系统建模与验证方法

摘要

形式化方法的系统设计、验证以及自动代码生成已经在单核系统上形成很多研究成果,但在多核并发系统上的研究仍面临许多科学问题.多核并发系统验证的难点在于验证者需要考虑多核并发系统中线程穿插执行造成的不确定性.本文基于Event-B形式化方法,提出了一种基于共享变量的组合推理方法解决多核并发系统验证中线程交互的不确定性问题.通过并发队列的验证实验,证明了该方法的有效性和正确性.未来的工作会将此方法形成具体的验证框架,进行ARINC653多核分区操作系统标准的验证.