文章基本信息

标题：Type-based Self-stabilisation for Computational Fields
本地全文：下载
作者：Ferruccio Damiani ; Mirko Viroli
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2015
卷号：11
期号：4
页码：1
DOI：10.2168/LMCS-11(4:21)2015
出版社：Technical University of Braunschweig
摘要：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.
其他关键词：Computational field, Core calculus, Operational semantics, Spatial computing, Type-based analysis, Type soundness, Type system, Refinement type