Vérification formelle
Qu’est-ce que la vérification formelle?
La vérification formelle est une technique permettant de vérifier que les systèmes remplissent les propriétés sélectionnées avec une certitude totale. Par exemple, pour un système de contrôle ferroviaire, on peut vérifier que les signaux ne peuvent pas afficher des aspects verts si certaines aiguilles ne sont pas dans la bonne position.
Alors que les tests sur de gros systèmes ne peuvent jamais atteindre une couverture complète, en raison du nombre de combinaisons à tester, la vérification formelle offre une certitude absolue, car elle utilise un raisonnement mathématique sans lacune.
Plusieurs gestionnaires d’infrastructure exigent maintenant que la vérification formelle soit appliquée pour évaluer la sécurité d’un système. Même lorsqu’ils ne sont pas obligés, les fournisseurs choisissent maintenant d’effectuer une vérification formelle en raison de la sécurité accrue et de la possibilité de réduire les tests en trouvant des problèmes avec les techniques automatisées.
Ce que Prover peut vous offrir
Prover vérifie formellement, depuis près de 30 ans, des postes d’enclenchement à relais, des postes d’enclenchement informatisés (tels que Siemens Westrace, Ansaldo Microlok, Alstom iVPI, GE ElectroLogiXS, conceptions basées sur SCADE, etc.), des systèmes CBTC, des systèmes ETCS, des microprocesseurs, des systèmes embarqués dans les voitures, et bien plus.
Prover fournit des produits, de la formation et une assistance pour vous permettre de créer votre propre équipe et de réaliser des vérifications formelle. Nous vous assisterons lors de la préparation et nous serons présents si des services d’experts sont nécessaires.
Si vous préférez, notre équipe de services professionnels peut procéder à une vérification formelle de votre système à l’aide de l’ensemble de nos produits, adaptés à vos besoins. Tout écart à une exigence de sécurité vous est communiqué, ainsi que ses causes.
Produits Prover
La gamme de produits de vérification formelle de Prover est vaste et en croissance constante, pour aller au-delà des normes de l’industrie. Consultez la liste de nos derniers produits pour voir ce qui vous intéresse:
- Prover iLock: CAO de poste d’enclenchement, contenant simulation, vérification, vérification formelle, ainsi que génération de code embarqué et génération documentaire
- Prover Certifier: Générateur de preuves de sécurité certifiables CENELEC SIL-4
- PSL: model-checker capable de vérifier formellement les grands systèmes industriels
- Prover Extractor: crée et vérifie des bases de données à partir de dessins Microstation
- Prover Trident: suite complète de processus et d’outils pour l’automatisation de la conception de poste d’enclenchements
- SCADE FV: Vérification formelle CENELEC SIL-4 des systèmes construits avec SCADE
- LCF: langage spécifique au domaine adapté à l’ingénierie de la signalisation
- PiSPEC: langage formel dédié à l’ingénierie de la signalisationg
- HLL: langage formel de haut niveau qui inclut la logique des prédicats et prend en charge d’importantes fonctionnalités de programmation telles que les tableaux et les nombres