Méthodes
Formelles
Méthodes formelles
Le problème
Trouver un bogue une fois qu’un logiciel a été déployé peut coûter très cher. Selon le Systems Sciences Institute d’IBM, le coût pour corriger un bogue est 15 fois plus élevé durant la phase de mise à l’essai que durant la phase de conception, et jusqu’à 100 fois plus élevé durant la phase de maintenance. Et cela n’inclut pas les coûts et les répercussions sur les gens lorsqu’il s’agit de systèmes critiques sur le plan de la sécurité.
Depuis 40 ans, des activités de recherche et de développement sont menées dans les universités et les industries afin de créer des méthodes formelles, et ces méthodes sont maintenant utilisées à titre de technologies de vérification et de validation de pointe en réponse à la montée de la puissance informatique.
Les méthodes formelles sont trop prometteuses pour être ignorées, comparées aux méthodes de mise à l’essai et de prototypage classiques. L’utilisation d’outils puissants fondés sur la logique mathématique vous permet de garantir la sécurité de votre système à l’intérieur de contraintes définies et de découvrir les lacunes de votre système.
Produits et services
CS Canada détient le savoir-faire requis pour appliquer les méthodes formelles de façon très précise et efficace à des volets critiques de votre projet.
- Application des méthodes formelles à votre processus de développement
- Garantir que votre conception répond aux objectifs du système
- Déterminer les cas pathologiques difficiles à découvrir à l’aide des techniques classiques
- Déployer un système de spécification officiel
- Cerner les occasions d’appliquer les méthodes formelles dans tout le processus de développement
- Création d’entités mathématiques pour modeler votre système complexe
- Garantir que le modèle utilisé pour exécuter les solveurs de théorèmes des méthodes formelles est élaboré selon le niveau d’abstraction approprié
- Garantir que des objectifs de sécurité appropriés sont fixés
- Formation sur l’utilisation et le déploiement des outils de pointe des méthodes formelles durant votre processus
- Solveurs SAT/SMT, Z3Prover, NuSMV, UUPAAL, SparkPro
Avantages
Grâce à notre soutien, nos clients des industries aérospatiale et automobile peuvent mettre en œuvre les méthodes formelles rapidement et efficacement, et ainsi garantir la sécurité de leurs systèmes et des gens.
- Décèle les erreurs plus tôt dans le processus de développement (dès l’étape de la définition des besoins)
- Permet d’effectuer une évaluation plus complète qu’avec la méthode classique de mise à l’essai grâce à une approche mathématique plus approfondie
- Plus rapide et plus économique pour tous les processus
Pourquoi faire affaire avec CS Canada?
Afin de pouvoir relever ces défis en matière de sécurité des systèmes critiques sur le plan de la sécurité, CS Canada a mis sur pied une équipe hautement qualifiée possédant une vaste expérience dans le développement, la vérification et la validation de logiciels temps réel critiques.
Réalisations de notre équipe :
- Expérience dans la sécurité et l’application de méthodes formelles dans les secteurs automobile et aérospatial
- Participation à divers projets, comme l’ADAS (système d’aide à la conduite), afin de démontrer l’utilisation des méthodes formelles
LIRE AUSSI
Brochure
Méthodes formelles
