Méthodes formelles

Pour le développement, la spécification et la validation de systèmes électroniques en logiciel ou en matériel, les méthodes formelles utilisent la modélisation mathématique. Ces méthodes formelles garantissent que ces systèmes peuvent être développés sans erreur. La base mathématique qui sous-tend les méthodes formelles est utilisée pour aider à garantir l'adéquation de la conception afin d'obtenir une fonctionnalité, une cohérence et une fiabilité réelles dans le produit final. Comme dans d'autres domaines de l'ingénierie, les méthodes formelles appliquent les mathématiques à l'ingénierie logicielle et matérielle afin d'ajouter de la certitude à la conception et aux tests de ces systèmes. Les méthodes formelles sont utilisées pour décrire les fonctions d'un système avant sa conception à l'aide de langages descriptifs garantissant la fonctionnalité du système. En fonction de la rigueur avec laquelle le système a été décrit, les méthodes formelles peuvent être utilisées pour le développement. Comme guide pour les exigences, des spécifications formelles peuvent être utilisées. Les méthodes formelles sont une description des fonctions qui peuvent être utilisées pour vérifier la validité du programme.

Il existe de nombreuses façons de mettre en œuvre les méthodes formelles. Certaines méthodes formelles sont trop coûteuses, en particulier pour les systèmes complexes ou les conceptions qui ont un niveau d'importance élevé. Dans ces cas, des erreurs pourraient entraîner des refabrications et des reconceptions coûteuses. Souvent, les méthodes formelles ne sont utilisées que pour décrire la fonction souhaitée et pour guider le développement. On parle alors de niveau 0 ou de méthodes formelles allégées. Le niveau 1 est celui où les méthodes formelles sont utilisées en plus de la vérification des fonctions. Le niveau 2, le plus haut degré de méthodes formelles, est celui où le système complet est vérifié par machine à travers toutes ses fonctions. Quelques exemples de systèmes qui pourraient être entièrement spécifiés par des méthodes formelles sont les semi-conducteurs complexes tels que les CPU ou les GPU ou les systèmes critiques dans les logiciels tels que ceux utilisés dans SCADA pour le contrôle des centrales électriques.