Extension d'ABAReL par les Propriétés d'Exécution
Résumé
Dans un travail antérieur, nous avons proposé une annexe comportementale ABAReL (AADL Behavioral Annex based on generalized Rewriting Logic), basée sur la logique de réécriture révisée, décrivant le composant "thread AADL" tout en préservant sa syntaxe initiale. Un modèle mathématique représenté par une théorie de réécriture décrivant son comportement simplifié, a été alors validé et implémenté sous l'environnement Maude. L'objectif de cet article est de raffiner l'annexe ABAReL et l'enrichir par d'autres constructions formelles de la logique de réécriture, à travers une extension de son langage Maude qui est RT-Maude (Real Time Maude). Cet enrichissement permettra de décrire les modes et les propriétés relatives au temps d'exécution théorique (la période, la politique d'expédition, etc.), déclarées dans le composant thread et leur prise en compte lors de son exécution. L'approche de formalisation proposée offre un cadre sémantique général, approprié pour raisonner sur le comportement de ces unités d'exécution concurrentes et pour pouvoir ensuite les analyser en tirant profit des outils existant autour de Maude.