Type-based self-stabilisation for computational fields

DOI10.2168/LMCS-11(4:21)2015zbMATH Open1448.68336arXiv1509.05659OpenAlexW2230770203MaRDI QIDQ3460426FDOQ3460426

Authors: Ferruccio Damiani, Mirko Viroli 

Publication date: 7 January 2016

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: Emerging network scenarios require the development of solid large-scale situated systems. Unfortunately, the diffusion/aggregation computational processes therein often introduce a source of complexity that hampers predictability of the overall system behaviour. Computational fields have been introduced to help engineering such systems: they are spatially distributed data structures designed to adapt their shape to the topology of the underlying (mobile) network and to the events occurring in it, with notable applications to pervasive computing, sensor networks, and mobile robots. To assure behavioural correctness, namely, correspondence of micro-level specification (single device behaviour) with macro-level behaviour (resulting global spatial pattern), we investigate the issue of self-stabilisation for computational fields. We present a tiny, expressive, and type-sound calculus of computational fields, and define sufficient conditions for self-stabilisation, defined as the ability to react to changes in the environment finding a new stable state in finite time. A type-based approach is used to provide a correct checking procedure for self-stabilisation.

Full work available at URL: https://arxiv.org/abs/1509.05659

Recommendations

• A higher-order calculus of computational fields
• Asynchronous distributed execution of fixpoint-based computational fields
• Distributed Computing - IWDC 2003
• Self-stabilization
• Self-stabilizing extensions for message-passing systems

zbMATH Keywords

type systemoperational semanticstype soundnessspatial computingcomputational fieldcore calculusrefinement typetype-based analysis

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (5)

• Topological Self-Stabilization with Name-Passing Process Calculi
• Asynchronous distributed execution of fixpoint-based computational fields
• A higher-order calculus of computational fields
• From distributed coordination to field calculus and aggregate computing
• On a higher-order calculus of computational fields

Uses Software

• APMC
• Featherweight Java

This page was built for publication: Type-based self-stabilisation for computational fields

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460426)