AltaRica est un langage de modélisation de systèmes informatiques. Il est principalement utilisé en phase de conception pour construire un modèle formel correspondant aux spécifications. Cette correspondance doit elle même être prouvée, par exemple à l'aide d'un vérificateur de modèle.
AltaRica possède son propre outil de vérification nommé ARC. NuSMV est un outil de référence pour la vérification de modèle qui dispose de son propre langage de modélisation. Afin de comparer ces deux outils et de pouvoir facilement passer de l'un à l'autre, nous souhaitons disposer d'un traducteur d'AltaRica vers NuSMV et inversement.
Le modèle formel prouvé peut ensuite être utilisé pour dériver une implémentation. La méthode B fournit une approche basée sur des raffinements successifs permettant cette démarche. Nous souhaitons disposer d'un traducteur AltaRica vers B pour pouvoir produire des implémentations prouvées à partir de modèles AltaRica.
Les étudiants pourront s'inspirer de parties du code source des logiciels AltaRica et NuSMV.
A. Arnold, A. Griffault, G. Point and A. Rauzy. The AltaRica formalism for describing concurrent systems. Fundam. Inf. 40, issue 2-3, pages 109-124, IOS Press, 2000.
AltaRica. http://altarica.labri.fr
R. Cavada, A. Cimatti, C.A. Jochim, G. Keighren, E. Olivetti, M. Pistore, M. Roveri and A. Tchaltsev. NuSMV 2.5 User Manual. http://nusmv.fbk.eu/NuSMV/userman/v25/nusmv.pdf
NuSMV. http://nusmv.fbk.eu/