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

  • Yves Bontemps

Student thesis: Doc typesDocteur en Sciences


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.
la date de réponse20 avr. 2005
langue originaleAnglais
L'institution diplômante
  • Universite de Namur
SuperviseurPatrick HEYMANS (Jury), W. THOMAS (Jury), S. UCHITEL (Jury), Jean-Luc HAINAUT (Jury) & PIERRE-YVES SCHOBBENS (Promoteur)

Contient cette citation