Formal Stepwise Development of Scalable and Reliable Multiagent Systems

Formal Stepwise Development of Scalable and Reliable Multiagent Systems

Denis Grotsev, Alexei Iliasov, Alexander Romanovsky
Copyright: © 2012 |Pages: 17
DOI: 10.4018/978-1-60960-747-0.ch004
OnDemand:
(Individual Chapters)
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

Abstract

This chapter considers the coordination aspect of large-scale dynamically-reconfigurable multi-agent systems in which agents cooperate to achieve a common goal. The agents reside on distributed nodes and collectively represent a distributed system capable of executing tasks that cannot be effectively executed by an individual node. The two key requirements to be met when designing such a system are scalability and reliability. Scalability ensures that a large number of agents can participate in computation without overwhelming the system management facilities and thus allows agents to join and leave the system without affecting its performance. Meeting the reliability requirement guarantees that the system has enough redundancy to transparently tolerate a number of node crashes and agent failures, and is therefore free from single points of failures. The Event B formal method is used to validate the design formally and to ensure system scalability and reliability.
Chapter Preview
Top

Background: Event-B

Event-B (Abrial, 2010) is a state-based formal method inherited from Classical B (Abrial, 1996). It is an approach for realising industrial-scale developments of highly dependable software. The method has been successfully used in the development of several real-life applications. An Event-B development starts from creating a formal system specification. The basic idea underlying stepwise development in Event-B is to design the system implementation gradually, by a number of correctness preserving steps called refinements.

The unit of a development is a model. An Event-B model is made of the static part, called a context, and the dynamic part, called a machine. A context defines constants c, sets (user defined types) s, and declares their properties in axioms P and theorems T:

  • contextC

  • setss

  • constantsc

  • axiomsP(c, s)

  • theoremsT(c, s)

A machine is described by a collection of variables v, invariants I(c, s, v), an initialisation event RI(c, s, v') and a set of machine events E:

  • machineM

  • seesC

  • variablesv

  • invariantsI(c, s, v)

  • eventsE

Complete Chapter List

Search this Book:
Reset