A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices

TL;DR

This paper introduces a sound spatio-temporal Hoare logic tailored for verifying structured interactive programs with registers and voices, exemplified through a distributed termination detection protocol.

Contribution

It develops a novel Hoare-like logic for rv-systems and demonstrates its application via formal verification of a distributed protocol.

Findings

The logic effectively verifies properties of rv-systems.

The case study confirms the logic's practical applicability.

The approach bridges space-time duality in program verification.

Abstract

Interactive systems with registers and voices (shortly, "rv-systems") are a model for interactive computing obtained closing register machines with respect to a space-time duality transformation ("voices" are the time-dual counterparts of "registers"). In the same vain, AGAPIA v0.1, a structured programming language for rv-systems, is the space-time dual closure of classical while programs (over a specific type of data). Typical AGAPIA programs describe open processes located at various sites and having their temporal windows of adequate reaction to the environment. The language naturally supports process migration, structured interaction, and deployment of components on heterogeneous machines. In this paper a sound Hoare-like spatio-temporal logic for the verification of AGAPIA v0.1 programs is introduced. As a case study, a formal verification proof of a popular distributed termination detection protocol is presented.