Passer au contenu

Les méthodes formelles au secours des développeurs de logiciels embarqués

Les outils mathématiques d’Esterel Studio 3.0 permettent une détection et une correction des bugs plus rapides.

Accélérer le développement de logiciels embarqués en détectant les bugs au moment de la conception. Tel est le but d’Esterel Studio. A cet effet, le produit développé par Esterel Technologies s’appuie sur les méthodes formelles, une technique surtout maîtrisée par les universitaires et quelques rares SSII, comme Trusted Logic pour le cryptage. Au total, cinq outils composent Esterel Studio : un éditeur graphique, un simulateur interactif, un vérificateur formel, un générateur de code et un automate de documentation.

Simuler le fonctionnement du logiciel

partir de spécifications en langage naturel, les développeurs formalisent d’abord graphiquement le fonctionnement du logiciel. Ils peuvent ensuite le simuler en plaçant différents observateurs aux endroits stratégiques. Ces observateurs prennent la forme de descriptions schématiques de problèmes éventuels. Par exemple, que se passe-t-il si le téléphone reçoit un appel alors qu’il compose un numéro ? Le modèle est simulé afin de savoir si la situation peut se produire. Et, dans cette éventualité, Esterel Studio propose des modifications à opérer sur le logiciel pour la gérer. Pour éviter de simuler toutes les situations possibles, les vérificateurs utilisent des outils mathématiques de méthodes formelles (des algorithmes basés sur les diagrammes de décision binaires) pour ” prouver ” la validité de la description.Esterel Studio génère aussi automatiquement des scénarios de tests qui peuvent être réutilisés par des logiciels de test spécialisés. Enfin, l’outil compile directement le programme en langage C et produit des rapports d’activité aux formats RTF ou HTML, automatisant ainsi la documentation du modèle. Pour l’instant disponible pour Windows NT et Solaris, Esterel Studio devrait bientôt pouvoir fonctionner sous Linux. De plus, la prochaine version du produit prendra en compte le langage VHDL de Verilog pour les circuits embarqués.

🔴 Pour ne manquer aucune actualité de 01net, suivez-nous sur Google Actualités et WhatsApp.


Stéphanie Chaptal