Modeling the development of LOTOS specification
Modélisation du développement de spécifications LOTOS
Résumé
Not available
Notre travail s'inscrit dans les premières étapes du développement de logiciels concernant le passage d'un cahier des charges à une spécification formelle, dans le domaine des réseaux de télécommunications. Notre sujet consiste à étudier la modélisation des étapes de développement de spécifications en langage LOTOS. Le modèle utilisé, PROPLANE, a été préalablement établi pour d'autres domaines. Par le biais d'un nouveau domaine d'application, l'objectif à long terme de notre étude est d'évaluer le modèle PROPLANE et de proposer des améliorations si nécessaire. LOTOS est constitué d'une algèbre de processus et d'une algèbre de données. Nous nous sommes concentrés sur la construction des expressions de comportement, c'est-à-dire des processus, en ayant éventuellement recours aux données. Sous le modèle PROPLANE, toute évolution d'un développement est gérée par des operateurs de développement. Notre modélisation correspond ainsi à des définitions d'operateurs pouvant s'enchainer les uns aux autres. Nous distinguons les constructions architecturale et, comportementale, pour lesquelles les mécanismes utilisés en LOTOS diffèrent. L’architecture fait une large utilisation des operateurs de composition parallèle, avec lesquels il faut veiller à conserver des processus effectifs, voire réguliers. Nous définissons pour cela des notions telles que la rigidité. La construction comportementale demande de définir des opérateurs permettant de gérer le développement d'arbres de transitions, ainsi que le détail de ces transitions. La nouveauté de notre approche consiste à chercher à profiter des propriétés sémantiques des processus en cours de développement. Afin de supporter des lignes de construction incrémentale par réduction de l'indéterminisme, nous donnons une définition opérationnelle des relations d'extension et de réduction de processus. Il apparait que PROPLANE doit être étendu pour manipuler des propriétés temporelles sur les états de développement.