Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Mazzanti F. An abstract, on the fly framework for the verification of service-oriented systems. Martin Wirsing, Matthias Hölzl (eds.). (Lecture Notes in Computer Science, vol. 6582). Heidelberg: Springer, 2011.
In this chapter we present (some of) the design principles which have inspired the development of the CMC/UMC verification framework. The first of these is the need of an abstraction mechanism which allows to observe a model in terms of an abstract L2TS , therefore hiding all the unnecessary underlying details of the concrete computational model, while revealing only the details which might be important to understand the system behavior. The second of these is the need a Service-Oriented Logic (SocL ) which is an event and state based, branching-time, efficiently verifiable, parametric temporal logic, for the formal encoding of service-oriented properties. The third principle is the usefulness of an on-the-fly, bounded model-checking approach for an efficient, interactive analysis of service-oriented systems which starts from the early stages of the incremental system design.
URL: http://www.springerlink.com/content/325447104h728012/
DOI: 10.1007/978-3-642-20401-2_18
Subject Model Checking
Verifica formale
Service-oriented Systems
D.2.4 Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional