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

Thèse de l'étudiant: Doc typesDocteur en Sciences

Résumé

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 de réussite20 avr. 2005
langueAnglais
Institution diplomante
  • Université de Namur
SuperviseurPatrick Heymans (Jury), W. THOMAS (Jury), S. UCHITEL (Jury), Jean-Luc Hainaut (Jury) & Pierre-Yves Schobbens (Promoteur)

Citer ceci

Relating inter-agent and intra-agent specifications : the case of life sequence chart
Bontemps, Y. (Auteur). 20 avr. 2005

Thèse de l'étudiant: Doc typesDocteur en Sciences