Verification of Parametric System Designs

System designs are often modeled as sets of threads whose activations are controlled by a domain-specific scheduler. Especially in the early design phases, the interactions between the threads and the scheduler often depend on parameters (such as the duration of thread suspensions) for which a value is not available.In this paper, we tackle the verification of designs with parametric scheduler-thread interaction. We propose a new method, called Semi-Symbolic Scheduler/Symbolic Threads (S3ST), to prove that a design satisfies the specified assertions for all possible values of the interaction parameters. We build on Explicit-Scheduler/Symbolic- Threads (ESST), an effective technique for verifying designs with cooperative scheduling, that is however limited to the case of non-parametric interactions. As in ESST, S3ST analyzes each thread symbolically using lazy predicate abstraction. The key difference is in the way the scheduler is dealt with. In ESST, the scheduler is directly executed...