Travaux R&D
(Recherche & Développement)
CLEARSY mène des travaux de Recherche & Développement dans différents cadres : des projets financés (Europe, France ou région) et des projets internes. Le tableau ci-dessous retrace les derniers projets de recherche publics auquel CLEARSY a participé de manière active.
LES THÉMATIQUES
CES PROJETS DE RECHERCHE PERMETTENT D’ABORDER DES THÉMATIQUES NOUVELLES ET D’APPROFONDIR DES SUJETS INNOVANTS TELS QUE:
L’AUTOMATISATION ET NIVEAU DE CONFIANCE DU PROCESSUS DE PREUVE AUTOMATIQUE
La preuve mathématique de modèles B permet d’éviter les tests unitaires et une grande partie des tests d’intégration du logiciel résultant. Cette preuve mathématique est un processus non entièrement automatisé (une intervention humaine est nécessaire pour compléter certaines démonstrations) qui repose sur un seul outil (validé grâce à d’autres outils de preuve ainsi que grâce à des expertises humaines). La connexion à d’autres outils de preuve permet d’augmenter à la fois le taux de preuve automatique (diminuer les interventions humaines) et le niveau de confiance en les résultats (quand deux outils, développés avec des technologies différentes et par des équipes disjoints, arrivent de manière concomitante à la même conclusion positive).
L’EXTENSION DE LA VALIDATION FORMELLE DE DONNÉES CONSTANTES
La validation formelle de données constantes est appliquée aujourd’hui par la quasi intégralité des acteurs du monde ferroviaire, notamment pour la validation des données de voie. Elle permet de vérifier que le paramétrage d’un système, au sens le plus large du terme, est acceptable vis à vis de règles définissant cette acceptabilité. Les règles sont formalisées grâce au langage mathématique de B et la vérification d’acceptabilité réalisé par le model-checker ProB. Pour des besoins de sécurisation de la décision, un deuxième outil de vérification, PredicateB++, permet de confirmer une décision positive de ProB. Cette approche est en cours de déploiement intensif auprès de nombreux industriels du domaine ferroviaire. Le langage de modélisation des propriétés est étendu alors que les interfaces d’entrée et de sortie sont diversifiées.