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 L 2 TS, 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.
An abstract, on the fly framework for the verification of service-oriented systems
Gnesi S;Mazzanti F
2011
Abstract
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 L 2 TS, 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.File | Dimensione | Formato | |
---|---|---|---|
prod_203870-doc_45417.pdf
solo utenti autorizzati
Descrizione: contributo
Tipologia:
Versione Editoriale (PDF)
Dimensione
493.81 kB
Formato
Adobe PDF
|
493.81 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.