Interface-Based Specification and Verification of Concurrency Controllers

We present a modular approach to specification and verification of concurrencycontrollers by decoupling their behavior and interface specifications.The behavior specification of a concurrency controller defineshow its shared variables change their values whereas theinterface specification definesthe order in which a client thread should call its methods.We show that the concurrency controllers can bedesigned modularly by composing their interfaces.We separate the verification of the concurrency controllersfrom the verification of the threads that use them.For the verification of the concurrency controllers weuse infinite state verification techniques which enableus to verify controllers with parameterized constants andarbitrary number of user threads. We automaticallygenerate Java monitors from the concurrency controllerspecifications which preserve the verified properties.For the thread verificationwe use finite state program verification toolswhich enable us to verify Java threads without anyrestrictions. We show that the user threads canbe verified using stubs generated from the concurrencycontroller interfaces which improves the efficiency ofthe thread verification significantly.