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.
This is joint work with Michele Loreti.