Analysis of a scheduler for a CAD framework

摘要

The experience report describes a case study in which a key component of a software system was modeled and analyzed to better understand a proposed algorithm prior to implementation. A Promela model of a linear scheduler for a CAD framework was developed. The Spin simulator was used to debug the model and, later, to illustrate how the algorithm works in different scenarios. Additionally, the Spin verifier was used to check various safety and liveness properties. The study revealed a deficiency with the algorithm, as originally proposed. Subsequently, the modeling tools provided by Spin were used in devising solutions to the problems. Finally, the Promela model was modified and verified to be correct. The actual implementation of the scheduler involves a significant amount of message passing, multiple execution threads, and potentially huge data structures. By focusing on the interfaces between threads, restricting the system scope, and abstracting details of data structures and irrelevant computations, a very simple model was obtained, which nevertheless provides an accurate representation of the communication between threads. The paper describes the steps that were abstracted and highlights the restrictions imposed on the model.