Improving PROPLANE : A Specification Development Framework
Identifieur interne : 00CC93 ( Main/Merge ); précédent : 00CC92; suivant : 00CC94Improving PROPLANE : A Specification Development Framework
Auteurs : N. LévySource :
Abstract
Formal specifications are used in a wide variety of areas, especially where the integrity of systems is critical. Tools and methodologies mainly exist to aid the steps of verification and refinement. But little is done to assist the software engineer in the production of formal specifications, although the quality of the specification is crucial to the quality of the program derived from it. A framework has been proposed for modelling developments. In this framework, a development step is composed of a workplan, a product and links between them. Each new step is obtained by the application of a development operator, i.e.\ an operator which enables the incremental construction and modification of the specification. Capturing alternative definitions of particular concepts and strategies is made possible by the definition of libraries of such operators. We propose an improvement of the framework, redefining the links between the workplan and the product describing them by a meta-program. This meta-program describes the construction of the specification, is incrementally developed by application of the operators and its evaluation gives the specification itself. The paper presents the workplan-product model, the meta-language introduced and some development operators. An exemple of specification development is given.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 001990
- to stream Crin, to step Curation: 001990
- to stream Crin, to step Checkpoint: 002C48
Links to Exploration step
CRIN:levy95dLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="298">Improving PROPLANE : A Specification Development Framework</title></titleStmt><publicationStmt><idno type="RBID">CRIN:levy95d</idno><date when="1995" year="1995">1995</date><idno type="wicri:Area/Crin/Corpus">001990</idno><idno type="wicri:Area/Crin/Curation">001990</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001990</idno><idno type="wicri:Area/Crin/Checkpoint">002C48</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">002C48</idno><idno type="wicri:Area/Main/Merge">00CC93</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Improving PROPLANE : A Specification Development Framework</title><author><name sortKey="Levy, N" sort="Levy, N" uniqKey="Levy N" first="N." last="Lévy">N. Lévy</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="4257">Formal specifications are used in a wide variety of areas, especially where the integrity of systems is critical. Tools and methodologies mainly exist to aid the steps of verification and refinement. But little is done to assist the software engineer in the production of formal specifications, although the quality of the specification is crucial to the quality of the program derived from it. A framework has been proposed for modelling developments. In this framework, a development step is composed of a workplan, a product and links between them. Each new step is obtained by the application of a development operator, i.e.\ an operator which enables the incremental construction and modification of the specification. Capturing alternative definitions of particular concepts and strategies is made possible by the definition of libraries of such operators. We propose an improvement of the framework, redefining the links between the workplan and the product describing them by a meta-program. This meta-program describes the construction of the specification, is incrementally developed by application of the operators and its evaluation gives the specification itself. The paper presents the workplan-product model, the meta-language introduced and some development operators. An exemple of specification development is given.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00CC93 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00CC93 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= CRIN:levy95d
|texte= Improving PROPLANE : A Specification Development Framework
}}
| This area was generated with Dilib version V0.6.33. |  |