Mathieu Martin

PSIRE 2005

Réingénierie pédagogique d'un logiciel de vérification formelle (2005)

Dans le contexte du génie logiciel, les méthodes formelles consistent en l'utilisation d'une notation mathématique dans le but de pouvoir vérifier et valider formellement les spécifications d'un logiciel. Il existe deux cours à l'ÉTS qui couvrent ce thème : MGL806 à la maîtrise et LOG310 au baccalauréat. Dans ces deux cours, nous utilisons un logiciel récent, peu adapté au contexte de l'enseignement. Le présent projet PSIRE vise à combler cette lacune afin d'offrir aux étudiants comme aux professeurs en génie logiciel, un outil convivial et utile pédagogiquement. Les modifications et les ajouts que nous désirons effectuer vise à : 1) favoriser les interactions en classe ; 2) encourager l'expérimentation ; 3) susciter la réflexion et aiguiser le sens critique de l'étudiant.

Les modifications proposées favorisent la création d'exemples « à la volée » et la modification rapides d'exemples existants, la création de scénarios de vérification modulaires et la validation des hypothèses de l'étudiant par la génération de contre-exemples suggérés, trois aspects essentiels pour soulever une véritable discussion en classe ou en laboratoire.