تقرير
A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices
| العنوان: | A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices |
|---|---|
| المؤلفون: | Dragoi, Cezara, Stefanescu, Gheorghe |
| سنة النشر: | 2008 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Programming Languages, Computer Science - Logic in Computer Science, F.1.2, F.3, D.2.4, D.3.2 |
| الوصف: | 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. Comment: 21 pages, 8 figures, Invited submission for WADT'08 LNCS Proceedings |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/0810.3332 |
| رقم الأكسشن: | edsarx.0810.3332 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |