Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Counterexample Guided Synthesis of Monitors for Realizability Enforcement
verfasst von : Matthias Güdemann, Gwen Salaün, Meriem Ouederni
Erschienen in: Automated Technology for Verification and Analysis
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Many of today’s software systems are built using distributed services, which evolve in different organizations. In order to facilitate their integration, it is necessary to provide a
contract
that the services participating in a composition should adhere to. A contract specifies interactions among a set of services from a global point of view. One important problem in a top-down development process is figuring out whether such a contract can be implemented by a set of services, obtained by projection and communicating via message passing. It was only recently shown, that this problem, known as
realizability
, is decidable if asynchronous communication (communication via FIFO buffers) is considered. It can be verified using the
synchronizability
property. If the system is not synchronizable, the system is not realizable either. In this paper, we propose a new, automatic approach, which enforces both synchronizability and realizability by generating
local
monitors through successive equivalence checks and refinement.