PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Mazzanti F., Gnesi S. CMC-UMC: a framework for the verification of abstract service-oriented properties. In: SAC'09 - 24th Annual ACM Symposium on Applied Computing (Honolulu, Hawaii, USA, 9-12 Marzo 2009). Proceedings, pp. 2111 - 2117. ACM, 2009.
 
 
Abstract
(English)
CMC and UMC are two prototypical instantiations of a common logical verification framework for the analysis of functional properties of service-oriented systems. The service-oriented SocL logic is used to describe the required system properties. Computational models of the system can be built either using the COWS specification language or designing the system as a collection of interacting UML state machines, and an on-the-fly model checker can be used to verify the satisfaction of the requirements and possibly to generate counterexamples or witnesses for them. An automotive case study is used to illustrate the overall framework.
URL: http://portal.acm.org/toc.cfm?id=1529282&type=proceeding&coll=GUIDE&dl=GUIDE&CFID=31953764&CFTOKEN=19553601
DOI: http://doi.acm.org/10.1145/1529282.1529751
Subject Service-Oriented Computing
Model checking
D.2.4 Software/Program Verification. Model checking


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