Modélisation des systèmes

Tout d’abord, les objectifs sont de présenter des concepts, des techniques et des outils pour développer des modèles d’un système cible qui respecte un ensemble de propriétés requises comme, par exemple, l’invariance, la sécurité et des propriétés d’éventualité.

Plus précisément, le cours aborde le paradigme de développement « correct par construction » qui est illustré par des applications industrielles. La construction de modèles nécessite de vérifier la cohérence de ces modèles et des outils tels que des assistants à la preuve, des model-checkers ou des simulateurs sont utilisés pour évaluer la qualité des modèles développés. En outre, des techniques pour produire des modèles corrects par construction introduits.

Le cours illustre le paradigme « correct par construction » en utilisant le framework RODIN et le langage de modélisation Event B.