Relating inter-agent and intra-agent specifications : the case of life sequence chart

  • Yves Bontemps

Student thesis: Doc typesDoctor of Sciences

Abstract

The problem of relating inter-agent and intra-agent behavioral specifications is investigated. These two views are complimentary, in that the former is closer to scenario-based user requirements whereas the latter is design-oriented. We use a graphical, user-friendly and very simple language as inter-agent specification language: Live Sequence Charts (LSC). LSC is presented and its properties are investigated: it is highly succinct, but inexpressive. There are essentially two ways to relate inter-agent and intra-agent specifications: (i) by checking that an intra-agent specification is correct with respect to some LSC specification and (ii) by automatically building an intra-agent specification from an LSC specification. Several variants of these problems exist: closed/open systems and centralized/distributed systems. We give inefficient but optimal algorithms solving all problems, besides synthesis of open distributed systems, which we show is undecidable. All the problems considered are difficult, even for a very restricted subset of LSCs, without alternatives, interleaving, conditions nor loops. We investigate the cost of extending the language with control flow constructs, conditions, real-time and symbolic instances. An implementation of the algorithms is proposed. The applicability of the language is illustrated on a real-world case study.
Date of Award20 Apr 2005
Original languageEnglish
Awarding Institution
  • University of Namur
SupervisorPatrick HEYMANS (Jury), W. THOMAS (Jury), S. UCHITEL (Jury), Jean-Luc HAINAUT (Jury) & PIERRE-YVES SCHOBBENS (Supervisor)

Keywords

  • LSC
  • Software Engineering
  • Live Sequence Charts
  • Distributed Systems
  • Scenarios
  • Synthesis
  • Verification
  • Game Theory
  • Formal Methods

Cite this

'