Where academic tradition
meets the exciting future

Formal Goal-Oriented Development of Resilient MAS in Event-B

Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, Formal Goal-Oriented Development of Resilient MAS in Event-B. TUCS Technical Reports 1033, Turku Centre for Computer Science, 2012.

Abstract:

Goal-Oriented Development facilitates structuring complex requirements. To ensure resilience the designers should guarantee that the system achieves its goals despite changes, e.g., caused by failures of system components. In this paper we propose a formal goal-oriented approach to development of resilient MAS. We formalize the notion of goal and goal achievement in Event-B and propose the specification and refinement patterns that allow us to guarantee that the targeted goals are reached despite agent failures. We illustrate our approach by a case study – development of an autonomous multi-robotic system.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tPeTrLa12a,
  title = {Formal Goal-Oriented Development of Resilient MAS in Event-B},
  author = {Pereverzeva, Inna and Troubitsyna, Elena and Laibinis, Linas},
  number = {1033},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2012},
  keywords = { Event-B, formal modelling, refinement, goal-oriented development, multi-agent system},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication