Proof Transformations for Evolutionary Formal Software Development
Identifieur interne : 001799 ( Istex/Curation ); précédent : 001798; suivant : 001800Proof Transformations for Evolutionary Formal Software Development
Auteurs : Axel Schairer [Allemagne] ; Dieter Hutter [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: In the early stages of the software development process, formal methods are used to engineer specifications in an explorative way. Changes to specifications and verification proofs are a core part of this activity, and tool support for the evolutionary aspect of formal software development is indispensable. We describe an approach to support evolution of formal developments by explicitly transforming specifications and proofs, using a set of predefined basic transformations. They implement small and controlled changes both to specifications and to proofs by adjusting them in a predictable way. Complex changes to a specification are achieved by applying several basic transformations in sequence. The result is a transformed specification and proofs, where necessary revisions of a proof are represented by new open goals.
Url:
DOI: 10.1007/3-540-45719-4_30
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001818
Links to Exploration step
ISTEX:67E5E63B2D0AA038A42D9D9C2881A5B71CF57BA9Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Proof Transformations for Evolutionary Formal Software Development</title><author><name sortKey="Schairer, Axel" sort="Schairer, Axel" uniqKey="Schairer A" first="Axel" last="Schairer">Axel Schairer</name><affiliation wicri:level="1"><mods:affiliation>German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, 66123, Saarbrücken, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, 66123, Saarbrücken</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: schairer@dfki.de</mods:affiliation><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Hutter, Dieter" sort="Hutter, Dieter" uniqKey="Hutter D" first="Dieter" last="Hutter">Dieter Hutter</name><affiliation wicri:level="1"><mods:affiliation>German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, 66123, Saarbrücken, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, 66123, Saarbrücken</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: hutter@dfki.de</mods:affiliation><country wicri:rule="url">Allemagne</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:67E5E63B2D0AA038A42D9D9C2881A5B71CF57BA9</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45719-4_30</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-4Q843DQQ-N/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001818</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001818</idno><idno type="wicri:Area/Istex/Curation">001799</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Proof Transformations for Evolutionary Formal Software Development</title><author><name sortKey="Schairer, Axel" sort="Schairer, Axel" uniqKey="Schairer A" first="Axel" last="Schairer">Axel Schairer</name><affiliation wicri:level="1"><mods:affiliation>German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, 66123, Saarbrücken, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, 66123, Saarbrücken</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: schairer@dfki.de</mods:affiliation><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Hutter, Dieter" sort="Hutter, Dieter" uniqKey="Hutter D" first="Dieter" last="Hutter">Dieter Hutter</name><affiliation wicri:level="1"><mods:affiliation>German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, 66123, Saarbrücken, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, 66123, Saarbrücken</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: hutter@dfki.de</mods:affiliation><country wicri:rule="url">Allemagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In the early stages of the software development process, formal methods are used to engineer specifications in an explorative way. Changes to specifications and verification proofs are a core part of this activity, and tool support for the evolutionary aspect of formal software development is indispensable. We describe an approach to support evolution of formal developments by explicitly transforming specifications and proofs, using a set of predefined basic transformations. They implement small and controlled changes both to specifications and to proofs by adjusting them in a predictable way. Complex changes to a specification are achieved by applying several basic transformations in sequence. The result is a transformed specification and proofs, where necessary revisions of a proof are represented by new open goals.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001799 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 001799 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:67E5E63B2D0AA038A42D9D9C2881A5B71CF57BA9
|texte= Proof Transformations for Evolutionary Formal Software Development
}}
| This area was generated with Dilib version V0.6.33. |  |