Formal Modeling of Socio-technical Collective Adaptive Systems

Socio-technical collective adaptive systems (CAS) are composed of different heterogeneous parts or entities (e.g., individuals, groups, computers, robots, agents, devices, software, services, sensors) that interact collectively in a complex and largely unpredictable manner. Their ability to be adaptive requires incorporating mechanisms that allow entities to interact and perform actions favoring the emergence of a global desired behavior or service. Therefore, analyzing and discovering new emerging behaviors and/or unexpected abnormal behaviors, as well as new opportunities of services emergence, require methods and tools for formally specifying, verifying, and validating foundational properties at design time and while running (runtime verification). In this paper, three emerging formal methods-situation calculus, ambient calculus, and bigraphical reactive systems-are first studied to shed more light on their appropriateness for specifying and verifying socio-technical CAS. A case study is used and its formal model using these methods is presented to show their fundamental features and limitations for modeling these systems.