| Le but de cet ouvrage est de définir une algèbre de processus ACTC pour formaliser les méthodes de spécification et vérification d'interfaces matérielles basées sur les chronogrammes hiérarchiques ou HAAD (de l'anglais Hierarchical Annotated Action Diagrams). Les HAAD sont un formalisme graphique qui permet de représenter des interfaces matérielles par des modules de base qui sont ensuite composés avec des opérateurs de composition hiérarchiques.; On dénote par interface matérielle tout système qui assure la communication de composants informatiques interconnectés, par des processus de communications spécifiques. La communication est établie par l'exécution d'événements, appelés actions. Une interface matérielle est un système temps-réel, c'est à dire un système qui doit produire ses résultats à l'intérieur d'intervalles de temps spécifiés par un ensemble de contraintes temporelles .; L'algèbre de processus ACTC est définie à partir d'un langage de spécification avec une syntaxe précise, dont les éléments sont appelés termes. Parmi les particularités de ce langage, spécifiquement conçu pour répondre aux besoins des développeurs d'interfaces matérielles, on note le support du dualisme des actions d'entrée et de sortie , des contraintes temporelles min, max, et conjonctives de type supposition, ou de type engagement, (en anglais “assume/commit contraints”), et du principe de causalité dans la sémantique de divers opérateurs de composition, tels que les contraintes temporelles réactives, la composition parallèle temporelle avec communication, le choix retardé temporisé , et l'opérateur d'exception temporisé. Dans le langage les opérateurs de composition parallèle, avec ou sans communication, et de choix, simple ou retardé, sont d'arité arbitraire.; Nous associons au langage une représentation équationnelle et une représentation opérationnelle. La spécification équationelle permet de déduire des égalités de termes d'une manière purement syntaxique à partir d'un ensemble de règles de déduction et un ensemble A d'égalités de base, appelé axiomatisation. Autrement dit, on définit une relation d'équivalence syntaxique de termes, décidable à partir de la spécification équationnelle du langage. La représentation opérationnelle est définie par un ensemble de règles de sémantique opérationnelle structurée à la manière de Plotkin [74] et permet d'associer à, tout terme un modèle opérationnel qui est un système de transitions étiquetées ou STE.; Nous définissons une relation d'équivalence sémantique ou opérationnelle ≈ sur le langage , à partir de critères sémantiques définis sur les modè... |
