Title: Verification of distributed systems involving bounded-time migration

Authors: Bogdan Aman; Gabriel Ciobanu

Addresses: Institute of Computer Science, Romanian Academy, Bld. Carol I, No. 8, 700505, Iaşi, Romania ' Institute of Computer Science, Romanian Academy, Bld. Carol I, No. 8, 700505, Iaşi, Romania

Abstract: We introduce and study a prototyping language for real-time distributed systems involving bounded-time migration and communication. The time constraints of this language are expressed as bounded intervals given by real numbers used to model faithfully the uncertainty of the delay in migration and communication of processes placed at explicit locations of a distributed system. We provide the operational semantics of this language and illustrate the new language by an example. Due to a translation of the bounded real-time distributed systems described in rTIMO into a network of timed safety automata, we can use an existing software tool for analysing their qualitative and quantitative properties.

Keywords: distributed system; bounded-time; migration; verification.

DOI: 10.1504/IJCCBS.2017.088400

International Journal of Critical Computer-Based Systems, 2017 Vol.7 No.3, pp.279 - 301

Accepted: 24 Aug 2017
Published online: 05 Dec 2017 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article