Concurrent usage control implementation verification using the SPIN model checker

Abstract

The UCON A usage control authorization model supports concurrency and the model left issue of synchronizing usage control processes to the implementation. Manual verification of application specific concurrent usage control implementation is a hard problem. In this paper, we show the usage of a formal verification tool, the SPIN model checker, for verifying the correctness of the concurrent usage control implementation. We also provide an illustrative case study. © 2010 Springer-Verlag Berlin Heidelberg.