Many digital systems are designed as collections of asynchronous processes orchestrated by a domain-specific scheduler. The verification of such scheduler-restricted asynchronous systems (SRA) is challenging due to process-process and process-scheduler interactions. In this paper, we tackle the problem of verifying configurable SRA. A configurable SRA describes an unbounded family of possible SRA, each resulting from an instantiation satisfying given configuration constraints; our goal is proving at once that every legal instantiation of a configurable SRA is correct. We propose a contract-based, deductive verification approach that combines (i) compositional proof rules that abstract the scheduler to prove top-level invariant properties, (ii) automatic summarizations of the methods invoked by the scheduler, (iii) simplification with respect to the nature of the space of configurations. The approach is grounded in (object-oriented) first order logic, requires reasoning over quantified statements, and leverages the Dafny software verifier as a backend. An experimental evaluation on industrial case studies demonstrates that the framework scales effectively and enables practical reasoning about complex parameterized behaviors.

翻译：许多数字系统被设计为异步进程的集合，这些进程由特定领域的调度器编排。由于进程间及进程与调度器间的交互，对此类调度器约束的异步系统（SRA）的验证具有挑战性。本文研究可配置SRA系统的验证问题。可配置SRA描述了一个无界的可能SRA族系，其中每个实例均满足给定的配置约束；我们的目标是一次性证明可配置SRA的每个合法实例化都是正确的。我们提出了一种基于合约的演绎验证方法，该方法结合了：（i）抽象调度器以证明顶层不变性属性的组合式证明规则；（ii）对调度器调用的方法进行自动汇总；（iii）基于配置空间特征的简化。该方法以（面向对象的）一阶逻辑为基础，需要对量化语句进行推理，并利用Dafny软件验证器作为后端。对工业案例的实验评估表明，该框架具有有效的可扩展性，并能够对复杂参数化行为进行实际推理。