Istituto di Scienza e Tecnologie dell'Informazione     
Ciancia V., Latella D., Massink M. An attribute-based front-end for FlyFast. Technical report, 2015.
TypicalCollectiveAdaptiveSystems(CAS)consistofalarge number of interacting objects that coordinate their activities in a decen- tralised and often implicit way. The design of such systems is challenging. It requires scalable analysis tools and techniques to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean-Field Approximated Model-checking. In particu- lar, the FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interac- tion paradigm. In this paper we present an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is presented and proved correct.
Subject Collective Adaptive Systems
Probabilistic Model-Checking
On-the-fly Model-Checking
Mean-Field Approximation
Discrete Time Markov Chains
Program Transformation
B.8.2 Performance Analysis and Design Aids
D.2.4 Software/Program Verification
F.1.2 Modes of Computation
F.3.1 Specifying and Verifying and Reasoning about Programs
39-XX Difference and functional equations
60Jxx Markov processes

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