Istituto di Scienza e Tecnologie dell'Informazione     
Bortolussi L., Cabri G., Di Marzo Serugendo G., Galpin V., Hillston J., Lanciani R., Massink M., Tribastone M., Weyns D. Verification of CAS. In: Dagstuhl Reports (ISSN: 2192-5283) V.4 n. 3/12 - Dagstuhl Publishing. 2014.
Verification is the process of assessing how well a system meets a specification or requirement. A variety of approaches have appeared in the literature, ranging from model checking to static analysis of source code and theorem proving. In this working group, we primarily focused on verification based on model checking, in which a state-based description of the system is assessed with respect to a property expressed in an appropriate specification language, like a temporal logic. In particular, we considered the challenges that arise in the model checking of Complex Adaptive Systems (CAS), which are systems comprised of a large number of heterogeneous agents which, interacting together, produce a complex array of collective behaviours. In our working group in Dagstuhl, we first identified the major issues and more interesting challenges that arise in the process of verification of CAS. Afterwards, we divided in two subgroups to discuss in detail specific topics related to this general framework. In particular, we chose to investigate: (1) the quantitative or stochastic model checking in the presence of uncertainty, and (2) the specifications and logics which capture the spatial arrangements of systems, characterising the impact of those arrangements on collective behaviour. A brief account of each subgroup is given below.
URL: http://drops.dagstuhl.de/opus/volltexte/2015/5006/
DOI: http://dx.doi.org/10.4230/DagRep.4.12.68
Subject Mean-field approximation
Probabilistic model-checking
On-the-fly model-checking
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
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