Computer Science – Programming Languages
Scientific paper
2008-10-19
Computer Science
Programming Languages
21 pages, 8 figures, Invited submission for WADT'08 LNCS Proceedings
Scientific paper
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.
Dragoi Cezara
Stefanescu Gheorghe
No associations
LandOfFree
A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-232052