Open Nets, Contexts and Their Properties.
Michele Loreti
Abstract
Klaim (A Kernel Language for Agents Interaction an Mobility) is a
simple formalism that can be used to model and program mobile
systems. It is based on process algebras but makes use of Linda-like
asynchronous communication and models distribution via multiple shared
tuple spaces. Tuple spaces and processes are distributed over
different localities and the classical Linda operations are indexed
with the location of the tuple space they operate on. For establishing
properties of Klaim Nets, we have designed a logic that is based on
HML but has richer action predicates that permit reasoning on the
information transmitted over the net and has state formulae for
testing the presence of specific tuples at given localities.
In the talk, after introducing Klaim and its logic, we shall present a
framework for specifying contexts for Klaim nets and an approach that
permits establishing properties of systems of which only some
components are fully known and a limited knowledge is available of the
context in which the known components are operating. By relying on a
notion of agreement of a net N with respect to a context specification
C[..], we shall guarantee that if a context specification is partially
instantiated (implemented) as a concrete net while guaranteeing
agreement between specification and implementation, then all formulae
satisfied by the more abstract description are satisfied also by the
refined one.