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.

Formulae meet Programs over the Net: a Framework for Reliable Network Aware Programming / L. BETTINI; R. DE NICOLA; M. LORETI. - In: AUTOMATED SOFTWARE ENGINEERING. - ISSN 0928-8910. - STAMPA. - 11:(2004), pp. 245-288. [10.1023/B:AUSE.0000028536.34044.47]

Formulae meet Programs over the Net: a Framework for Reliable Network Aware Programming

BETTINI, LORENZO;LORETI, MICHELE
2004

Abstract

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.
2004
11
245
288
L. BETTINI; R. DE NICOLA; M. LORETI
File in questo prodotto:
File Dimensione Formato  
ase.pdf

Accesso chiuso

Tipologia: Versione finale referata (Postprint, Accepted manuscript)
Licenza: Tutti i diritti riservati
Dimensione 1.37 MB
Formato Adobe PDF
1.37 MB Adobe PDF   Richiedi una copia

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/213228
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact