Mobile Calculi based on Domains


Open Nets Contexts and Their Properties

R. {De Nicola} and M. Loreti

Abstract

KLAIM (A Kernel Language for Agents an Mobility) is a simple formalism that can be used to model and program mobile systems; it allows programmers to concentrate on the distributed structure of programs while ignoring their precise physical allocations. For establishing properties of KLAIM Nets, a logic based on HML was defined. This logic permits specifying properties related to resource allocation, security and behaviours. A weakness of the approach is that, in order to use KLAIM and its associated logic to establish nets properties one needs to have a full implementation of the system under consideration. This is a very strong assumption when dealing with wide area networks, because very often, only a fragment of the system is known and a limited knowledge of the overall context is available. In the paper, after recalling KLAIM and its logic, we shall present a framework for specifying contexts for KLAIM. Then, by relying on a notion of agreement, we shall set up a framework ensuring that, whenever an abstract specification is partially implemented as a concrete net (guaranteeing agreement with specifications) all formulae satisfied by the more abstract description are satisfied also by the refined one.

@Unpublished\{de-nicola.loreti:open-nets-contexts-properties,
  author = \{R. {De Nicola} and M. Loreti},
  title = \{Open Nets Contexts and Their Properties},
  year = \{2004}, 
  note = \{submitted}, 
  url = \{http://mikado.di.fc.ul.pt/repository/de-nicola.loreti_open-nets-contexts-properties.pdf}
}


About this site. Last modified: Fri Sep 22 08:16:22 CEST 2017