A MODEL-BASED DESIGN-FOR-VERIFICATION APPROACH TO CHECKING FOR DEADLOCK IN MULTI-THREADED APPLICATIONS
Beata Sarna-Starosta, R. E. Kurt Stirewalt, Laura K. Dillon · International Journal of Software Engineering and Knowledge Engineering · 2007
This paper explores an approach to design for verification in systems built atop a middleware framework which separates synchronization concerns from the "core-functional logic" of a program. The framework is based on a language-independent compositional model of synchronization contracts, called Szumo, which integrates well with popular OO design artifacts and provides strong guarantees of non-interference for a class of strictly exclusive systems. An approach for extracting models from Szumo design artifacts and analyzing the generated models to detect deadlocks is described. A key decision was to use Constraint Handling Rules to express the semantics of synchronization contracts, which allowed a transparent model of the implementation logic.