Méthode formelle (informatique)

Résumé

En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique ou du matériel électronique numérique, afin de démontrer leur validité par rapport à une certaine spécification. Elles reposent sur les sémantiques des programmes, c'est-à-dire sur des descriptions mathématiques formelles du sens d'un programme donné par son code source (ou, parfois, son code objet). Ces méthodes permettent d'obtenir une très forte assurance de l'absence de bug dans les logiciels (Evaluation Assurance Level, Safety Integrity Level). Elles sont utilisées dans le développement des logiciels les plus critiques. Leur amélioration et l'élargissement de leurs champs d'application pratique sont la motivation de nombreuses recherches scientifiques en informatique. Exemple Comment vérifier que l'identité (a+b)^2 = a^2 + b^2 + 2(a*b) est correcte ? Une vérification naïve pourrait consister

Source officielle

https://fr.wikipedia.org/wiki/M%C3%A9thode_formelle_(informatique)

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (75)

Chargement

Afficher plus

Publications associées

Chargement

Personnes associées (2)

Personnes associées

Chargement

Unités associées (2)

Unités associées

Chargement

Concepts associés (39)

Concepts associés

Chargement

Cours associés (20)

Cours associés

Chargement

Séances de cours associées (20)

Séances de cours associées

Chargement

Publications associées (75)

Formal Development and Validation of the DSGamma System Based on CO-OPN/2 and Coordinated Atomic Actions

The objectives of this research are twofold. On the first hand, it aims to show the interest of Coordinated Atomic actions (CA actions) as a design concept and, on the other hand it explains how the formal language COOPNTWO can be used to express a CA action design. A real distributed application is developed according to a simple development life cycle: informal requirements, specification, design, implementation. The design phase is built according to the CA action concept. The COOPNTWO language is used to express the specification, and design phase. The implementation is made in Java based on a library of generic classes adapted to CA action concepts. The validation phase is briefly addressed, in order to demonstrate the extent to which the development methodology followed in this paper can be useful for proving properties.

1998

Chargement

As hardware designs get more robust and efficient, software can solve a wider range of challenges, each one more advanced than the previous one. The direct consequence is that software complexity grows continuously. Despite being used more frequently in development processes, traditional testing frameworks are not enough to avoid flaws in programs. Moreover, many company concerned by the security of their applications, especially in mission critical industries, spend a considerable effort and amount of money to write robust software certified by solid guidelines and standards. For embedded systems, MISRA C is a certification process commonly used which provides directives to write portable and maintainable C code while avoiding many pitfalls of the language. Leon takes an orthogonal approach by providing tools for formal verification of programs written in a subset of Scala. In a previous work we introduced GenC, a module for Leon that converts Scala applications into equivalent and safe C99 programs, allowing developers to leverage high-level feature of Scala to implement robust applications, even for embedded systems. The aim of this project is to augment Leon and GenC in order to support a larger fragment of Scala that includes inheritance, generic programming, additional numeric types, pattern matching and more. Additionally, we closely analyse the MISRA Guidelines and shape the generated C code to work towards compliance with its rules while taking advantage of the verification capabilities of Leon to automatically detect a variety of bugs. We discuss these improvements and new features by implementing the famous LZW compression/decompression algorithm as well as a kernel-based image processing algorithm and show that the produced native C programs are significantly more efficient both in terms of memory usage but also in terms of execution speed.

2017

Chargement

Supporting Loop Proofs in KeY by using BLAST

Mathias Krebs

In contrast to beta-testing, formal verification can guarantee correctness of a program against a specification. Two basic verification techniques are theorem proving and model checking. Both have strengths and weaknesses. Theorem proving is powerful, but difficult to use for a software engineer. Model checking is fully automatic, but less powerful and hard to extend. This paper shows a possibility, how to combine both approaches, in order to surround the weaknesses. Concretely, we automatize the proof of while loops in the theorem prover KeY, by using the model checker BLAST.

2006

Chargement

Afficher plus