A MODEL-BASED DESIGN-FOR-VERIFICATION APPROACH TO CHECKING FOR DEADLOCK IN MULTI-THREADED APPLICATIONS
| Autor: | Laura K. Dillon, R. E. K. Stirewalt, Beata Sarna-Starosta |
|---|---|
| Rok vydání: | 2007 |
| Předmět: |
Constraint Handling Rules
Computer Networks and Communications Programming language Semantics (computer science) Computer science Distributed computing Deadlock computer.software_genre Computer Graphics and Computer-Aided Design Artificial Intelligence Middleware Synchronization (computer science) Constraint logic programming Model-based design Key (cryptography) computer Software |
| Zdroj: | International Journal of Software Engineering and Knowledge Engineering. 17:207-230 |
| ISSN: | 1793-6403 0218-1940 |
| DOI: | 10.1142/s0218194007003197 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|