S9 SIIA Interaction et Vérification

Présentation

La composition est un problème crucial du logiciel. Nous l’abordons ici sous l’angle de sa spécification sous la forme de contrats pour décrire les comportements attendus et offerts puis de la vérification de ses contrats à l’aide de l’approche dite model-checking.

Pré-requis nécessaires

Modélisation, Sémantique

Descriptif

Programme (20h) :

La notion d’interface et de contrat (SysML, contrat niveau sémantique pré/post, OCL, contrat niveau synchronisation interactions)

Modélisation des interactions (statecharts, automates, sémantiques de la synchronisation )

Sémantique des automates temporisés

Logiques temporelles (type LTL et CTL) pour la spécifications
de propriétés

Techniques et algorithmes pour le model-checking

Illustration avec le langage le model-checker UPPAAL

Modalités de contrôle des connaissances

Session 1 ou session unique - Contrôle de connaissances

Nature de l'enseignementModalitéNatureDurée (min.)NombreCoefficientRemarques
CMCCTravaux Pratiques100%

Session 2 : Contrôle de connaissances

Nature de l'enseignementModalitéNatureDurée (min.)NombreCoefficientRemarques
CMCTEcrit et/ou Oral1100%