Compositional Checking of Communication among Observers

Autor:	Hans-Dieter Ehrich, Ralf Pinger
Rok vydání:	2001
Předmět:	Model checking Object-oriented programming Correctness Common Object Request Broker Architecture Programming language Computer science Concurrency Temporal logic System requirements specification computer.software_genre Algorithm computer
Zdroj:	Fundamental Approaches to Software Engineering ISBN: 9783540418634 FASE
DOI:	10.1007/3-540-45314-8_4
Popis:	Observers are objects inside or outside a concurrent object system carrying checking conditions about objects in the system (possibly including itself). In a companion paper [EP00], we show how to split and localise checking conditions over the objects involved so that the local conditions can be checked separately, for instance using model checking. As a byproduct of this translation, the necessary communication requirements are generated, taking the form of RPC-like action calls (like in a CORBA environment) among newly introduced communication symbols. In this paper, we give an algorithmic method that matches these communication requirements with the communication pattern created during system specification and development. As a result, correctness of the latter can be proved. In case of failure, the algorithm gives warnings helping to correct the communication specification.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::04c1c320609e5360f277afa59297d73a https://doi.org/10.1007/3-540-45314-8_4 Zobrazit plný text záznamu