This paper proposes an approach to modelling and analysis of distributed real-time actor systems, which is based on the UPPAAL statistical model checker (SMC). SMC was chosen because it automatizes simulations, offers a temporal logic language to formalize specifications and exploits statistical techniques to infer quantitative measures about a model. The approach is integrated in a system life-cycle where a same model can be transitioned without distortions from analysis down to design and implementation, currently based on Java. The paper describes the adopted actor modelling language and its architectural framework, illustrates the UPPAAL SMC approach and demonstrates its practical usefulness through a running example.

Statistical Model Checking of Distributed Real-Time Actor Systems

Libero Nigro
Membro del Collaboration Group
;
Paolo F. Sciammarella
Membro del Collaboration Group
2017-01-01

Abstract

This paper proposes an approach to modelling and analysis of distributed real-time actor systems, which is based on the UPPAAL statistical model checker (SMC). SMC was chosen because it automatizes simulations, offers a temporal logic language to formalize specifications and exploits statistical techniques to infer quantitative measures about a model. The approach is integrated in a system life-cycle where a same model can be transitioned without distortions from analysis down to design and implementation, currently based on Java. The paper describes the adopted actor modelling language and its architectural framework, illustrates the UPPAAL SMC approach and demonstrates its practical usefulness through a running example.
2017
Distributed timed actors, timing constraints, control framework, statistical model checking, UPPAAL SMC
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/270372
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 2
social impact