PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F. A state/event-based model-checking approach for the analysis of abstract system properties. In: Science of Computer Programming, vol. 76 (2) pp. 119 - 135. Elsevier, 2011.
 
 
Abstract
(English)
We present the UMC framework for the formal analysis of concurrent systems specified by collections of UML state machines. The formal model of a system is given by a doubly labelled transition system, and the logic used to specify its properties is the state-based and event-based logic UCTL. UMC is an on-the-fly analysis framework which allows the user to interactively explore a UML model, to visualize abstract behavioural slices of it and to perform local model checking of UCTL formulae. An automotive scenario from the service-oriented computing (SOC) domain is used as case study to illustrate our approach.
URL: http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6V17-50NBNJ5-2&_user=3967543&_coverDate=02%2F01%2F2011&_rdoc=1&_fmt=high&_orig=search&_origin=search&_sort=d&_docanchor=&view=c&_acct=C000061181&_version=1&_urlVersion=0&_userid=3967543&md5=9e64ba3
DOI: 10.1016/j.scico.2010.07.002
Subject Formal methods
UML State machines
Temporal logic
Model checking
Automotive systems Service-oriented computing
Service-oriented computing
D.2.4 Software/Program Verification. Model Checking
D.2.4 Software/Program Verification. Formal methods
F.4.1 Mathematical Logic. Temporal logic


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