On Formal Methods for Collective Adaptive System Engineering. {Scalable Approximated, Spatial} Analysis Techniques. Extended Abstract

TL;DR

This paper discusses the role of formal methods in system engineering, presenting two novel analysis techniques—scalable population model-checking and spatial model-checking—supported by software tools, within the context of the QUANTICOL project.

Contribution

It introduces two new formal analysis techniques for collective adaptive systems, with supporting tools, advancing scalable and spatial analysis methods in system engineering.

Findings

Developed scalable population DTMC model-checking technique.

Created spatial model-checking for closure spaces.

Supported by software tools within the QUANTICOL project.

Abstract

In this extended abstract a view on the role of Formal Methods in System Engineering is briefly presented. Then two examples of useful analysis techniques based on solid mathematical theories are discussed as well as the software tools which have been built for supporting such techniques. The first technique is Scalable Approximated Population DTMC Model-checking. The second one is Spatial Model-checking for Closure Spaces. Both techniques have been developed in the context of the EU funded project QUANTICOL.