Vers un développement formel non incrémental
| Autor: | Pham, Thi-Kim-Dung, Dubois, Catherine, Levy, Nicole |
|---|---|
| Přispěvatelé: | Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), University of Engineering and Technology, Vietnam National University, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux (SAMOVAR), Institut Mines-Télécom [Paris] (IMT)-Télécom SudParis (TSP) |
| Jazyk: | francouzština |
| Rok vydání: | 2016 |
| Předmět: | |
| Zdroj: | AFADL 2016 : 15èmes journées des Approches Formelles dans l'Assistance au Développement de Logiciels AFADL 2016 : 15èmes journées des Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2016, Besançon, France. Edités par Aurélie Hurault et Nicolas Stouls, pp.106-113 |
| Popis: | International audience; Modularité, généricité, héritage sont des mécanismes qui facilitent le développement et la vérification formelle de logiciels corrects par construction en permettant de réutiliser des spécifications, du code et/ou des preuves. Cependant les lignes de produits exploitent d'autres techniques de réutilisation ou de modification graduelle. Les méthodes formelles permettant la production de code correct par construction (en B ou FoCaLiZe par exemple) ne sont pas bien adaptées à la variabilité telle qu'elle apparaît dans les lignes de produits. Nous proposons d'approcher ce problème par la définition d'un langage formel, GFML, proche de la variabilité mise en oeuvre dans les lignes de produits permettant de spécifier, implanter et prouver. Ce langage est compilé vers un formalisme existant, ici FoCaLiZe. Cet article illustre par l'exemple une des constructions offertes par GFML ainsi que sa traduction en FoCaLiZe |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|