This article proposes an approach to modelling and analysis of distributed probabilistic timed actors. The approach rests on a lightweight infrastructure of actors -Theatre- whose design aims to favoring the development of predictable time-dependent applications. Adopted actors are thread-less and their evolution is transparently regulated by a customizable control layer which has a reflective link with the application. A Theatre system consists of a collection of interacting computing nodes (theatres) each one hosting a sub system of local actors. The control layers of the various theatre components coordinate each other so as to enforce a common global time notion (real or simulated time). The abstract Theatre modelling language can be reduced in a case to Uppaal, which opens to the analysis of the functional/non-functional aspects of a distributed system. A key factor of the reduction process concerns the possibility of making both a non-deterministic analysis of an actor model (checking that something, e.g., an event, can occur), and a quantitative evaluation of system behavior by statistical model checking of the same model (e.g., estimating the probability for an event to occur). The paper describes the Theatre architecture and introduces a real-time case study which is used as a running example throughout the paper. The operational semantics of Theatre is provided and the proposed reduction of Theatre actors on top of Uppaal detailed through the chosen example. Some experimental results are reported about qualitative and quantitative analysis of the case study. Finally, conclusions are presented with an indication of further work.

Qualitative and quantitative model checking of distributed probabilistic timed actors

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

Abstract

This article proposes an approach to modelling and analysis of distributed probabilistic timed actors. The approach rests on a lightweight infrastructure of actors -Theatre- whose design aims to favoring the development of predictable time-dependent applications. Adopted actors are thread-less and their evolution is transparently regulated by a customizable control layer which has a reflective link with the application. A Theatre system consists of a collection of interacting computing nodes (theatres) each one hosting a sub system of local actors. The control layers of the various theatre components coordinate each other so as to enforce a common global time notion (real or simulated time). The abstract Theatre modelling language can be reduced in a case to Uppaal, which opens to the analysis of the functional/non-functional aspects of a distributed system. A key factor of the reduction process concerns the possibility of making both a non-deterministic analysis of an actor model (checking that something, e.g., an event, can occur), and a quantitative evaluation of system behavior by statistical model checking of the same model (e.g., estimating the probability for an event to occur). The paper describes the Theatre architecture and introduces a real-time case study which is used as a running example throughout the paper. The operational semantics of Theatre is provided and the proposed reduction of Theatre actors on top of Uppaal detailed through the chosen example. Some experimental results are reported about qualitative and quantitative analysis of the case study. Finally, conclusions are presented with an indication of further work.
2018
Modelling and verification; Model checking; Statistical model checking; Actors; Asynchronous message passing; Timing constraints; Probabilistic behavior; Uppaal
File in questo prodotto:
File Dimensione Formato  
nigro-SIMPAT-2018.pdf

accesso aperto

Descrizione: Publisher version is available at: https://www.sciencedirect.com/science/article/abs/pii/S1569190X18301035; DOI: 10.1016/j.simpat.2018.07.011
Tipologia: Documento in Pre-print
Dimensione 474.3 kB
Formato Adobe PDF
474.3 kB Adobe PDF Visualizza/Apri

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/285110
 Attenzione

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

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 23
  • ???jsp.display-item.citation.isi??? 15
social impact