Preuves de systèmes réactifs dans le modèle synchrone

Julien Musset (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs

Prouver la correction de programmes informatiques devient une contrainte importante dans la réalisation de logiciels. Les systèmes réactifs se développent comme modèles de gestion de flots de données. Le but de ce travail est de proposer une spécification logique de tels systèmes afin de prouver des propriétés grâce au système de démonstration automatique SPIKE.

Mots clés: automatic proof; synchronous language; lustre; démonstration automatique; flux de données; dataflow; synchrone

Domaines: Autre [cs.OH]

Julien Musset. Preuves de systèmes réactifs dans le modèle synchrone. [Stage] 99-R-300 || musset99a, 1999, 30 p. ⟨inria-00098855⟩