LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Languages: French
Types: Article
Subjects: Exigences, Agents, Rôles, Multi-stratégies, Raffinement de stratégies, 000, Requirements, Roles, Multi-strategies, Strategy refinement
Ces travaux concernent la modélisation formelle d’exigences et les interactions entre agents. Nous y avons développé un langage de modélisation pour les exigences d’un système à élaborer, KHI. En s’inspirant notamment des méthodes KAOS et TROPOS-i*, KHI synthétise les concepts essentiels relatifs aux buts et aux agents. Il permet en particulier d’exprimer la question de la capacité effective des agents à assurer la satisfaction des spécifications qui leurs sont assignées. Nous appelons cette question le problème de l’assignation. Dans KHI, nous exprimons ce problème comme la question de la satisfaction d’un certain nombre de critères de correction par un modèle. Pour donner un formalisme aux concepts de KHI et un moyen de résolution du problème de l’assignation, nous introduisons également une logique temporelle multi-agents, USL. Elle s’inspire des travaux dans le domaine, en particulier ATL*sc et SL. Comme ces derniers formalismes, elle utilise des contextes de stratégies pour exprimer des capacités d’agents à assurer la satisfaction de propriétés temporelles. Elle se distingue des autres formalismes existants principalement par deux aspects : d’abord elle utilise des stratégies non-déterministes. Nous les appelons des multi-stratégies. Nous pouvons ainsi exprimer des propriétés de raffinement entre les multi-stratégies. Par ailleurs, nous utilisons pour USL des exécutions du système qui ne sont pas nécessairement infinies. Nous pouvons alors formaliser les notions d’engagement contradictoire pour un agent et de capacités d’actions conflictuelles pour un ensemble d’agents. Nous réduisons ensuite la satisfaction des critères de correction qui expriment le problème de l’assignation dans KHI à des instances du problème de model-checking pour une version adéquate de USL, USLKHI . Nous donnons un algorithme de résolution pour ce problème, il tourne en espace polynomial. L’ensemble des concepts et des outils présentés est par ailleurs illustré par un cas d’étude décrivant des missions d’observation spatiale. These studies relate to modeling languages for requirements engineering. The aim is to provide tools for the evaluation of agents' capacity to ensure the satisfaction of their assigned specifications (we talk of "the assignment problem"). To do so, we first develop a modeling language (Khi). Then we give a set of assignment correctness criteria for systems that are modelled as instances of Khi. We also develop a formal tool, USLKhi, for wich we solve the model checking problem. We reduce the different correctness criteria for Khi instances to instances of the model checking problem for USLKhi. Thus as a whole, our proposition enables to express, formalise and solve the assignment problem. We also illustrate the set of concepts and tools that are presented with a case study featuring spatial observation missions.
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article