Serveur d'exploration sur la recherche en informatique en Lorraine

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

Code Generation From Hierarchical Concurrency Specifications

Identifieur interne : 009531 ( Main/Merge ); précédent : 009530; suivant : 009532

Code Generation From Hierarchical Concurrency Specifications

Auteurs : Denis Roegel ; Scott Smolka

Source :

RBID : CRIN:roegel01a

English descriptors

Abstract

This paper explains how executable Java code is generated from hierarchical specifications in the Concurrency Factory specification and verification environment. Besides the ability to generate executable code from verified, abstract concurrency specifications, the paper's main contributions include : (1) new solutions to the well-known input/output guard-scheduling problem in the context of hierarchically configured concurrent systems ; (2) code-generation algorithms that produce both thread-based Java code and distributed ADA code ; (3) the use of the Concurrency Factory itself to verify an abstraction of each generated code module ; in this sense, the Factory is self-verifying ; and, finally, (4) a report on our experience in executing the generated code for simulation and debugging purposes in the case of the Rether real-time ethernet protocol.

Links toward previous steps (curation, corpus...)


Links to Exploration step

CRIN:roegel01a

Le document en format XML

<record>
<TEI>
<teiHeader>
<fileDesc>
<titleStmt>
<title xml:lang="en" wicri:score="314">Code Generation From Hierarchical Concurrency Specifications</title>
</titleStmt>
<publicationStmt>
<idno type="RBID">CRIN:roegel01a</idno>
<date when="2001" year="2001">2001</date>
<idno type="wicri:Area/Crin/Corpus">003109</idno>
<idno type="wicri:Area/Crin/Curation">003109</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">003109</idno>
<idno type="wicri:Area/Crin/Checkpoint">001626</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">001626</idno>
<idno type="wicri:Area/Main/Merge">009531</idno>
</publicationStmt>
<sourceDesc>
<biblStruct>
<analytic>
<title xml:lang="en">Code Generation From Hierarchical Concurrency Specifications</title>
<author>
<name sortKey="Roegel, Denis" sort="Roegel, Denis" uniqKey="Roegel D" first="Denis" last="Roegel">Denis Roegel</name>
</author>
<author>
<name sortKey="Smolka, Scott" sort="Smolka, Scott" uniqKey="Smolka S" first="Scott" last="Smolka">Scott Smolka</name>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc>
<textClass>
<keywords scheme="KwdEn" xml:lang="en">
<term>code generation</term>
<term>proofs</term>
<term>specification</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front>
<div type="abstract" xml:lang="en" wicri:score="2560">This paper explains how executable Java code is generated from hierarchical specifications in the Concurrency Factory specification and verification environment. Besides the ability to generate executable code from verified, abstract concurrency specifications, the paper's main contributions include : (1) new solutions to the well-known input/output guard-scheduling problem in the context of hierarchically configured concurrent systems ; (2) code-generation algorithms that produce both thread-based Java code and distributed ADA code ; (3) the use of the Concurrency Factory itself to verify an abstraction of each generated code module ; in this sense, the Factory is self-verifying ; and, finally, (4) a report on our experience in executing the generated code for simulation and debugging purposes in the case of the Rether real-time ethernet protocol.</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 009531 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 009531 | 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:roegel01a
   |texte=   Code Generation From Hierarchical Concurrency Specifications
}}

Wicri

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022