| BDL04 (Article)
|
| Author(s) | Lorenzo Bettini, Rocco De Nicola and Michele Loreti |
| Title | « Formulae meet Programs over the Net: a Framework for Correct Network Aware Programming » |
| Journal | Automated Software Engineering: Special Issue on Distributed and Mobile Software Engineering |
| Volume | 11 |
| Number | 3 |
| Page(s) | 245-288 |
| Year | 2004 |
| URL | http://rap.dsi.unifi.it/~bettini/bibliography/files/ase-fmp.ps.gz |
| Abstract |
| A general framework for network aware programming is presented that consists of a language for programming mobile applications, a logic for specifying properties of the applications and an automatic tool for verifying such properties. The framework is based on X-Klaim, eXtended Klaim, an experimental programming language specifically designed to program distributed systems composed of several components interacting through multiple tuple spaces and mobile code. The proposed logic is a modal logic inspired by Hennessy-Milner logic and is interpreted over the same labelled structures used for the operational semantics of X-Klaim. The automatic verification tool is based on a complete proof system that has been previously developed for the logic. |
@article{BDL04,
number = {3},
volume = {11},
author = {Bettini, Lorenzo and De Nicola, Rocco and Loreti, Michele},
url = {http://rap.dsi.unifi.it/~bettini/bibliography/files/ase-fmp.ps.gz},
title = {{Formulae meet Programs over the Net: a Framework for Correct Network
Aware Programming}},
abstract = {A general framework for network aware programming is presented
that consists of a language for programming mobile applications, a
logic for specifying properties of the applications and an
automatic tool for verifying such properties. The framework is
based on X-Klaim, eXtended Klaim, an experimental programming
language specifically designed to program distributed systems
composed of several components interacting through multiple tuple
spaces and mobile code. The proposed logic is a modal logic
inspired by Hennessy-Milner logic and is interpreted over the same
labelled structures used for the operational semantics of X-Klaim.
The automatic verification tool is based on a complete proof
system that has been previously developed for the logic.},
pages = {245-288},
year = {2004},
journal = {Automated Software Engineering: Special Issue on Distributed and
Mobile Software Engineering},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
