Open Nets Contexts and Their Properties
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: Wed Mar 4 17:53:56 CET 2020