Timed-Aware Proof Assistant for ASTD, CCSL and Event-B

Le numérique est désormais omniprésent dans nos activités quotidiennes. Nombreuses de nos actions sont numérisées, analysées et assistées par un ordinateur. Or, nous produisons de plus en plus de logiciels et les bugs (ou souvent les défauts de spécification) sont largement sous-estimés. La tendance en effet et à produire des mises à jour (parfois quotidiennes, souvent hebdomadaires) plutôt que de passer le temps nécessaire à développer un logiciel robuste et sûr. Tant que le logiciel reste sur un ordinateur qui manipule « seulement » des données, le risque reste limité. Quand le logiciel envahi nos hôpitaux, nos appartements, nos voitures, nos immeubles, cela pose un risque de sécurité majeur pour la société.

Notre projet s’intéresse à fournir un environnement de spécification formel pour une prise en compte systémique des exigences à la fois fonctionnelles et non fonctionnelles de tels logiciels dits critiques. Il vise à tirer profit de l’expertise des deux équipes qui y sont impliquées pour combiner assistant de preuve (Event-B) et modèles à la fois temporels et temporisés dans notre cas à travers les langages ASTD et CCSL.

Faculty Supervisor:

Marc Frappier

Student:

Partner:

Université Côte Azur

Discipline:

Computer science

Sector:

Cyber Security; Technology; Other

University:

Université de Sherbrooke

Program: