Verifiable interactions in global computing environments. This project will investigate computational and logical models of individual and collective behaviour of computational entities - which we refer to as computees - interacting in the context of global and open computing environments. Currently, techniques for developing interactions in such environments result either in low-level implementations with no obvious logical characterisation, which are, therefore, not verifiable, or in abstract specifications possibly employing expressive modalities, but which are computationally intractable in many cases. To bridge this gap, SOCS aims at supplying models of complex interaction that not only allow formal specification and verification of properties but also lend themselves to concrete realisations which can be proven correct with respect to those models, without relying upon simulation techniques. Such properties may be local - within a single computing environment, or global - within a dynamic collection of open and connected sub-environments

(Societies of) Computees. Computees are abstractions of the entities that populate global computing environments. These entities can form complex organisations, which for the purposes of this project we call societies of computees. Such societies can be tightly knit with computees having pre-specified roles, objectives and tasks, with an obligation to resolve their conflicts. An example of such a society could be an air traffic management system, where different airlines, pilots and control centres work in a global and open environment. At the other extreme, a society can consist of loosely knit, heterogeneous computees, again with their own individual tasks and objectives, but with no overall obligation towards one another. An example of such a society is a group of business entities in a global trading environment, as encountered in electronic commerce applications.

Computees have their own knowledge, capabilities, resources, objectives and rules of behaviour. Each computee typically has only a partial, incomplete and possibly inaccurate view of the society and of the environment and of the other computees, and it might have inadequate resources or capabilities to achieve its objectives. In order to remedy these shortcomings, computees might have to perform hypothetical reasoning in order to fill gaps in their knowledge as well as to interact with other computees. This interaction may involve communication, coordination, and negotiation and may, but does not need to, conform to standards shared between computees. Hypothetical reasoning and interaction may lead to a need for the computees to revise their knowledge and their objectives

Societies have a global flavour in that they may be composed of vastly diverse computees, in the same way that human societies are composed of different individuals with different patterns of behaviour and culture. Societies evolve dynamically, with computees moving between societies with the passage of time. Therefore, computees need to adapt their behaviour and knowledge to these changes. This may involve assimilating new information about the behaviour and objectives of other computees in the new societies.

For the kind of societies of computees that we envisage, distributed computation comes naturally into play as each computee has its own (incomplete) knowledge base, and it needs to coordinate and cooperate with other computees to achieve individual or global objectives. This high-level view of distributed computation is fundamental to a global computing system whose behaviour can be verified, but it is orthogonal to lower-level distribution mechanisms, such as process synchronisation and mobility. In our view mobility is orthogonal to our high level view of a global computing system in that in our context the idea of mobility, i.e., migrating from one community to another, is not primarily motivated by efficiency issues, and is not necessarily related to the concept of physical location, as in classical mobility literature. Existing or forthcoming tools for mobility of code can be used, instead, as a possible means for extending, in an efficient way, our resulting system.

Back to : Objectives Menu