June 11, 2012

Christophe Chareton (Doctorant ONERA Toulouse) Début de l'exposé à 14h

Nous proposons des structures d’interprétation pour le langage KHI, un langage de modélisation pour l’ingénierie des exigences, qui formalise notamment les notions d’agents, de buts et d’opérations. Deux notions d’agents s’y confrontent : les acteurs, qui sont les agents présents et décrits par leurs capacités d’action sur le système, et les rôles, qui décrivent le comportement attendu des agents pour la réalisation des buts. Les rôles sont ensuite assignés à des acteurs ou des coalitions d’acteurs. La capacité effective des coalitions à jouer les rôles qui leur sont assignés fournit donc un critère de correction du modèle, on appelle le problème relatif problème de l’assignation. KHI a une sémantique formelle dans un fragment de la logique temporelle multi- agents ATL*, nommé ATLK HI . Nous décrivons les modèles sémantiques qui permettent d’interpréter ATLK HI et de réduire le problème de l’assignation à un problème de model-checking.