Une approche formelle de la reconfiguration dynamique

noteInternational audienceLes applications auto-adaptables modi?ent leur comportement de façon dynamiqueet autonome par le biais d’opérations d’introspection, de recomposition, d’ajout et suppressionde composants, dans le but de s’adapter aux changements pouvant survenir dans leur contexted’exécution. Un des moyens de favoriser leur robustesse est de disposer d’un support formelpermettant de modéliser ces applications, de spéci?er les programmes d’adaptation, d’y ex-primer des propriétés et de les véri?er. Nous proposons un cadre formel de spéci?cation et deraisonnement sur des programmes avec recon?guration dynamique inspiré du modèle à com-posants Fractal. Le cadre proposé, nommé FracL, est fondé sur une description axiomatiquedes primitives de Fractal en logique de premier ordre, et permet la spéci?cation et la preuvedes propriétés autant fonctionnelles que de contrôle dans ces systèmes. Notre modèle a été tra-duit dans l’atelier de spéci?cation et de preuve Focal, ce qui permet à la fois d’en assurer lacohérence et de fournir un cadre outillé pour raisonner sur des applications concrètes