Et si votre ordinateur pouvait comprendre vos exigences ?
Après le signal d’activation, la commande de freinage doit se stabiliser dans un délai court.
Deux lacunes séparent une exigence écrite d’un système sûr. Elles subsistent, quel que soit le nombre de tests exécutés.
Les exigences informelles ne sont pas interprétées de la même manière par tous les ingénieurs. « Rapide », « peu après », « stable » : chacun comble les imprécisions à sa façon. Même correctement implémentée, une exigence mal comprise conduit au mauvais système.
Les tests vérifient les comportements que vous avez pensé à essayer. Ils ne peuvent toutefois pas couvrir chaque entrée, chaque état et chaque paramètre. La véritable question — « mon exigence de sécurité peut-elle un jour être violée ? » — reste donc sans réponse, même lorsque toute la suite de tests est au vert.
Tester, c’est échantillonner. La vérification formelle apporte la preuve.
Les méthodes formelles comblent ces deux lacunes : précisez l’exigence, puis démontrez que le code la respecte.
BTC Universal Pattern est une méthode graphique et intuitive d’ingénierie des exigences : l’éditeur et la documentation constituent un seul et même artefact. Vous décrivez la propriété à respecter ; l’outil la traduit en langage machine et préserve à chaque étape la traçabilité jusqu’à l’exigence source.
Mettez en surbrillance les expressions significatives de l’exigence et transformez-les en macros réutilisables.
Organisez graphiquement les macros en déclencheur, action et délai : cette structure lève toute ambiguïté.
Liez chaque macro à des signaux système réels. L’exigence est désormais compréhensible par machine et exécutable.
Rédiger manuellement des spécifications formelles était complexe. La formalisation d’une exigence est fondamentalement une tâche linguistique, précisément un domaine dans lequel l’IA moderne excelle.
Le BTC AI Assistant propose un Universal Pattern à partir d’une exigence écrite — déclencheur, action et délai — que vous pouvez ensuite affiner, approuver ou utiliser pour générer des cas de test.
Exigences compréhensibles par la machine = vérification automatisée.
Chaque cas de test existant est vérifié simultanément par rapport à chaque exigence formalisée. Les effets secondaires qu’un test n’avait pas été conçu pour rechercher sont ainsi détectés sans effort supplémentaire.
La vérification de modèles génère précisément les cas de test qui manquent à votre suite et porte la couverture des exigences à 100 %, de manière déterministe plutôt que par tâtonnements.
La vérification de modèles produit une preuve mathématique qu’une exigence ne peut jamais être violée — aucune combinaison d’entrées ou de paramètres n’atteint l’état dangereux — ou fournit un contre-exemple concret.
La formalisation force la précision : des exigences vagues sont détectées avant que le code et les tests n’existent.
Une couverture des exigences mesurée et complétée automatiquement, plutôt qu’estimée.
Chaque test est vérifié par rapport à toutes les exigences : les régressions apparaissent sans effort supplémentaire.
Les vecteurs générés automatiquement comblent les lacunes jusqu’à une couverture complète des exigences.
Une garantie sur toutes les entrées et tous les paramètres.
Des tests reliés aux exigences, des résultats traçables jusqu’à leur source.
MC/DC et couverture structurelle avec analyse des écarts.
Comment la suite d’outils prend en charge le cycle de vie de la sécurité fonctionnelle.
Une licence d’évaluation inclut un atelier de démarrage avec nos ingénieurs, mis en œuvre de bout en bout à partir de l’une de vos exigences réelles.