Proving correctness of Timed Concurrent Constraint Programs

TL;DR

This paper introduces a temporal logic framework for verifying the correctness of timed concurrent constraint programs, enabling formal reasoning about their reactive behaviors in a compositional manner.

Contribution

It presents a novel temporal logic with modalities for specifying and proving correctness of timed concurrent constraint programs, including a sound and complete axiomatization.

Findings

Provides a formal logic for reasoning about reactive behaviors.

Enables compositional correctness proofs.

Achieves soundness and completeness in the axiomatization.

Abstract

A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These modalities provide an assumption/commitment style of specification which allows a sound and complete compositional axiomatization of the reactive behavior of timed concurrent constraint programs.