Système informatique (10), pour la validation formelle d’un système physique électronique ou électromécanique définissable par modélisation selon un principe d’ingénierie des systèmes, comportant un processeur (12), des moyens de stockage (14) et une plate-forme logicielle (16) constituée de plusieurs modules fonctionnels (18, 20, 22, 24, 26, 28, 30) stockés dans les moyens de stockage (14) et exécutables par le processeur (12), dans lequel : les moyens de stockage (14) comportent un espace de définition du système physique par enregistrement d’un ensemble structuré de spécifications techniques (32) exprimées dans un langage de modélisation prédéterminé ; la plate-forme logicielle (16) comporte un module fonctionnel (18) de génération de premiers modèles de validation (MV) à partir de l’ensemble structuré de spécifications techniques (32) et de propriétés de validation (P1, …, PN) ; caractérisé en ce que : la plate-forme logicielle (16) comporte un module fonctionnel solveur (20) conçu pour appliquer au moins un solveur (S2, S3) non applicable aux premiers modèles de validation ; pour chaque solveur (S2, S3) non applicable aux premiers modèles de validation, la plate-forme logicielle (16) comporte un module fonctionnel (24, 26) de génération, à partir de l’ensemble structuré de spécifications techniques (32), de requêtes (REQ’’) exécutables par ce solveur (S2, S3) pour la vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32) ; et la plate-forme logicielle (16) comporte en outre une interface (UI 20 ), associée au module fonctionnel solveur (20), dédiée à la sélection d’un solveur parmi ledit au moins un solveur (S2, S3). Système informatique (10) selon la revendication 1, dans lequel : le module fonctionnel solveur (20) est également conçu pour proposer un premier solveur (S1) applicable aux premiers modèles de validation (MV), pour une vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32) à partir des premiers modèles de validation (MV) ; et l’interface (UI 20 ) est dédiée à la sélection d’un solveur parmi le premier solveur (S1) et ledit au moins un solveur (S2, S3). Système informatique (10) selon la revendication 2, dans lequel la plate-forme logicielle (16) comporte, pour chaque autre solveur (S2, S3) que le premier solveur (S1), un module fonctionnel (28, 30) de traduction d’un résultat (RES’’) de la vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32) fourni par cet autre solveur (S2, S3) en un résultat (RES) dans un format tel qui aurait été fourni par le premier solveur (S1) à partir de l’ensemble structuré de spécifications techniques (32) pour la vérification des mêmes propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32). Système informatique (10) selon l’une quelconque des revendications 1 à 3, dans lequel chaque solveur (S1, S2, S3) est conçu pour produire une valeur booléenne de vérification de chaque propriété de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32) indiquant si cette propriété de validation est vérifiée ou non pour l’ensemble structuré de spécifications techniques (32). Système informatique (10) selon l’une quelconque des revendications 1 à 4, dans lequel l’ensemble structuré de spécifications techniques (32) est enregistré dans l’espace de définition du système physique sous une forme comportant au moins : un dictionnaire d’entrées du système physique prenant chacune la forme d’une paire formée d’une clé et d’une valeur associée à cette clé ; et un dictionnaire de sorties du système physique prenant chacune la forme d’une paire formée d’une clé et d’une valeur associée à cette clé, chaque sortie étant en outre associée à une liste d’au moins une relation logique de cause à effet formalisant le respect d’une propriété donnée. Système informatique (10) selon l’une quelconque des revendications 1 à 5, dans lequel pour au moins l’un (S3) dudit au moins un solveur (S2, S3) non applicable aux premiers modèles de validation, le module fonctionnel (26) de génération, à partir de l’ensemble structuré de spécifications techniques (32), de requêtes (REQ’’) exécutables par ce solveur (S3) pour la vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32) comporte : un sous-module fonctionnel (26A) de traduction des spécifications techniques (32) dans un format commun d’interprétation prédéterminé autre que le langage de modélisation prédéterminé ; un sous-module fonctionnel (26B) de génération de deuxièmes modèles de validation (MV’) à partir de l’ensemble structuré de spécifications techniques (32’) exprimées dans le format commun d’interprétation prédéterminé et des propriétés de validation (P1, …, PN) ; et le cas échéant un sous-module fonctionnel (26C) de génération, à partir des deuxièmes modèles de validation (MV’), desdites requêtes (REQ’’) exécutables par ce solveur (S3) pour la vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32). Système informatique (10) selon l’une quelconque des revendications 1 à 6, dans lequel pour au moins l’un (S2) dudit au moins un solveur (S2, S3) non applicable aux premiers modèles de validation, le module fonctionnel (24) de génération, à partir de l’ensemble structuré de spécifications techniques (32), de requêtes (REQ’’) exécutables par ce solveur (S2) pour la vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32) comporte : un sous-module fonctionnel (24A) de transformation de l’ensemble structuré de spécifications techniques (32) exprimées dans le langage de modélisation prédéterminé en un ensemble d’équations à arbres syntaxiques ; et un sous-module fonctionnel (24B) de génération, à partir de l’ensemble d’équations à arbres syntaxiques, desdites requêtes (REQ’’) exécutables par ce solveur (S2) pour la vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32). Système informatique (10) selon la revendication 7, dans lequel le sous-module fonctionnel de transformation (24A) comporte un analyseur logiciel syntaxique et lexical. Système informatique (10) selon la revendication 8, dans lequel le module fonctionnel (24) de génération de requêtes (REQ’’) exécutables par ce solveur (S2) est implémenté en langage de programmation Python et l’analyseur syntaxique et lexical comporte l’outil Python Lex-Yacc. Procédé de validation formelle d’un système physique électronique ou électromécanique définissable par modélisation selon un principe d’ingénierie des systèmes, comportant les étapes suivantes : modélisation (100) du système physique par enregistrement, dans un espace de définition du système physique inclus dans des moyens de stockage (14), d’un ensemble structuré de spécifications techniques (32) exprimées dans un langage de modélisation prédéterminé ; réception, par une plate-forme logicielle (16) exécutée par un processeur (12) ayant accès aux moyens de stockage (14), de l’ensemble structuré de spécifications techniques (32) ; sélection (102), à l’aide d’une interface dédiée (UI 20 ) associée à un module fonctionnel solveur (20) de la plate-forme logicielle (16), d’un solveur parmi : un éventuel premier solveur (S1) de vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32) à partir de premiers modèles de validation (MV), et au moins un autre solveur (S2, S3), non applicable aux premiers modèles de validation, pour lequel la plate-forme logicielle (16) comporte un module fonctionnel (24, 26) de génération (108, 110), à partir de l’ensemble structuré de spécifications techniques (32), de requêtes (REQ’’) exécutables par cet autre solveur (S2, S3) pour la vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32) ; génération (104), par un module fonctionnel (18) de la plate-forme logicielle (16), des premiers modèles de validation (MV) à partir de l’ensemble structuré de spécifications techniques (32) et de propriétés de validation (P1, …, PN) au moins lorsque l’éventuel premier solveur (S1) est sélectionné ; et exécution (114) du solveur sélectionné pour la vérification des propriétés de validation (P1, …, PN) de l’ensemble structuré de spécifications techniques (32). Programme d’ordinateur (16) téléchargeable depuis un réseau de communication et/ou enregistré sur un support (14) lisible par ordinateur (10) et/ou exécutable par un processeur (12), caractérisé en ce qu’il comprend des instructions (18, 20, 22, 24, 26, 28, 30) pour l’exécution des étapes d’un procédé de validation formelle d’un système physique selon la revendication 10, lorsque ledit programme (16) est exécuté sur un ordinateur (10).