Modelling and Analysis of Distributed Asynchronous Actor Systems Using THEATRE

被引：2

作者：

Nigro, Libero ^{[1
]}

Sciammarella, Paolo F. ^{[1
]}

机构：

[1] Univ Calabria, Dept Informat Modelling Elect & Syst Sci DIMES, Arcavacata Di Rende, CS, Italy

来源：

CYBERNETICS APPROACHES IN INTELLIGENT SYSTEMS: COMPUTATIONAL METHODS IN SYSTEMS AND SOFTWARE 2017, VOL. 1 | 2018年 / 661卷

关键词：

Model-driven development; Asynchronous distributed systems; Probabilistic and timed actors; Statistical model checking; UPPAAL;

D O I：

10.1007/978-3-319-67618-0_14

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

This paper introduces THEATRE, a modular software architecture whose aim is supporting modelling, analysis, design and implementation of distributed asynchronous probabilistic and timed/untimed actor systems. A key factor of THEATRE is that a same model can be transitioned without distortions from a development phase to the next one. The analysis phase is currently based on the UPPAAL Statistical Model Checker (SMC) which automatizes simulations, and uses statistical techniques (e.g., Monte Carlo-like and sequential hypothesis testing) to infer quantitative measures from the simulation runs. The design and implementation phases are based on Java. The paper describes the abstract modelling language of THEATRE and focusses on its translation to UPPAAL SMC. The approach is practically demonstrated by two modelling examples and their experimental analysis.

引用

页码：150 / 162

页数：13

共 16 条

[1]

Agha G., 1985, Actors: A Model of Concurrent Computation in Distributed Systems

[2] A THEORY OF TIMED AUTOMATA [J].

ALUR, R ;

DILL, DL .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235

[3]

Bellifemine F. L., 2007, Developing MultiAgent Systems with JADE

[4] Control centric framework for model continuity in time-dependent multi-agent systems [J].

Cicirelli, Franco ;

Nigro, Libero .

CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2016, 28 (12) :3333-3356

[5] Real-time specifications [J].

David, Alexandre ;

Larsen, Kim G. ;

Legay, Axel ;

Nyman, Ulrik ;

Traonouez, Louis-Marie ;

Wasowski, Andrzej .

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2015, 17 (01) :17-45

[6]

Hinton A, 2006, LECT NOTES COMPUT SC, V3920, P441

[7] SYMMETRY-BREAKING IN DISTRIBUTED NETWORKS [J].

ITAI, A ;

RODEH, M .

INFORMATION AND COMPUTATION, 1990, 88 (01) :60-87

[8] PTRebeca: Modeling and analysis of distributed and asynchronous systems [J].

Jafari, Ali ;

Khamespanah, Ehsan ;

Sirjani, Marjan ;

Hermanns, Holger ;

Cimini, Matteo .

SCIENCE OF COMPUTER PROGRAMMING, 2016, 128 :22-50

[9] Statistical model checking of Timed Rebeca models [J].

Jafari, Ali ;

Khamespanah, Ehsan ;

Kristinsson, Haukur ;

Sirjani, Marjan ;

Magnusson, Brynjar .

COMPUTER LANGUAGES SYSTEMS & STRUCTURES, 2016, 45 :53-79

[10] On the Power of Statistical Model Checking [J].

Larsen, Kim G. ;

Legay, Axel .

LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: DISCUSSION, DISSEMINATION, APPLICATIONS, ISOLA 2016, PT II, 2016, 9953 :843-862

← 1 2 →