Assume-Guarantee Reasoning with Scheduled Components

Contract-based assume-guarantee reasoning can be used to improve the scalability of model checking by decomposing complex verification problems. In previous work, we demonstrated this approach for systems modeled using the Architecture Analysis and Design Language (AADL) assuming a synchronous model of computation. This allows nondeterministic ordering of parallel components and generally results in an over-approximation of real behavior. This paper describes an approach to incorporating an execution schedule in the assume-guarantee reasoning. We define our semantic interpretation of contracts when components are executed according to this schedule, more accurately reflecting the behavior of the system implementation. We introduce virtual scheduling events which tie AADL timing and execution semantics to contracts. A case study based on a simple unmanned air vehicle surveillance system is provided to illustrate our approach.