Study of the Semantics of ``Real'' Parallel Languages in TLA
Identifieur interne : 001E51 ( Crin/Corpus ); précédent : 001E50; suivant : 001E52Study of the Semantics of ``Real'' Parallel Languages in TLA
Auteurs : Denis RoegelSource :
English descriptors
- KwdEn :
Abstract
In the first part, we wanted to ease the derivation of real concurrent programs from abstract specifications. We have defined an intermediate step (ctla) as a crossing between the specification language used, TLA+, and a real concurrent language such as CC++. We have kept the flexible and abstract data types of TLA+, and in the same time, we have added control structures which are closer to CC++. The whole semantics of the language has been defined within TLA+. Thus, a ctla program enters the refinement chain and can be subject to proofs. In the second part, we have studied TLA action nets. A net is a graphical representation of a structured execution. We have then defined a reduction operation on nets, whose purpose is to find a net equivalent to a given net, but simpler, in that the number of edges is smaller. The rewriting system that we proposed corresponds to elementary simplifications in the nets, and therefore in the concurrent programs which can correspond to nets. This system is confluent. When a net can be completely reduced to a TLA action, and if this net satisfies some simple constraints, we show that the computation represented by the net is observably equivalent to the execution of the action which is its reduction. Then, the reduction is a means to prove that an action is implemented by a structured group of actions.
Links to Exploration step
CRIN:roegel97aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="181">Study of the Semantics of ``Real'' Parallel Languages in TLA</title></titleStmt><publicationStmt><idno type="RBID">CRIN:roegel97a</idno><date when="1997" year="1997">1997</date><idno type="wicri:Area/Crin/Corpus">001E51</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Study of the Semantics of ``Real'' Parallel Languages in TLA</title><author><name sortKey="Roegel, Denis" sort="Roegel, Denis" uniqKey="Roegel D" first="Denis" last="Roegel">Denis Roegel</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>C++</term><term>Derivation of correct concurrent programs</term><term>TLA</term><term>concurrency</term><term>correctness</term><term>object-oriented languages</term><term>refinement</term><term>specification languages</term><term>temporal logic</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="3771">In the first part, we wanted to ease the derivation of real concurrent programs from abstract specifications. We have defined an intermediate step (ctla) as a crossing between the specification language used, TLA+, and a real concurrent language such as CC++. We have kept the flexible and abstract data types of TLA+, and in the same time, we have added control structures which are closer to CC++. The whole semantics of the language has been defined within TLA+. Thus, a ctla program enters the refinement chain and can be subject to proofs. In the second part, we have studied TLA action nets. A net is a graphical representation of a structured execution. We have then defined a reduction operation on nets, whose purpose is to find a net equivalent to a given net, but simpler, in that the number of edges is smaller. The rewriting system that we proposed corresponds to elementary simplifications in the nets, and therefore in the concurrent programs which can correspond to nets. This system is confluent. When a net can be completely reduced to a TLA action, and if this net satisfies some simple constraints, we show that the computation represented by the net is observably equivalent to the execution of the action which is its reduction. Then, the reduction is a means to prove that an action is implemented by a structured group of actions.</div></front></TEI><BibTex type="techreport"><ref>roegel97a</ref><crinnumber>97-R-125</crinnumber><category>15</category><equipe>MODEL</equipe><author><e>Roegel, Denis</e></author><title>Study of the Semantics of ``Real'' Parallel Languages in TLA</title><year>1997</year><type>Rapport de recherche</type><note>Traduction de thèse.</note><url>http://www.loria.fr/publications/1997/97-R-125/97-R-125.ps</url><keywords><e>Derivation of correct concurrent programs</e><e>refinement</e><e>correctness</e><e>specification languages</e><e>temporal logic</e><e>TLA</e><e>object-oriented languages</e><e>C++</e><e>concurrency</e></keywords><abstract>In the first part, we wanted to ease the derivation of real concurrent programs from abstract specifications. We have defined an intermediate step (ctla) as a crossing between the specification language used, TLA+, and a real concurrent language such as CC++. We have kept the flexible and abstract data types of TLA+, and in the same time, we have added control structures which are closer to CC++. The whole semantics of the language has been defined within TLA+. Thus, a ctla program enters the refinement chain and can be subject to proofs. In the second part, we have studied TLA action nets. A net is a graphical representation of a structured execution. We have then defined a reduction operation on nets, whose purpose is to find a net equivalent to a given net, but simpler, in that the number of edges is smaller. The rewriting system that we proposed corresponds to elementary simplifications in the nets, and therefore in the concurrent programs which can correspond to nets. This system is confluent. When a net can be completely reduced to a TLA action, and if this net satisfies some simple constraints, we show that the computation represented by the net is observably equivalent to the execution of the action which is its reduction. Then, the reduction is a means to prove that an action is implemented by a structured group of actions.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001E51 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 001E51 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Corpus
|type= RBID
|clé= CRIN:roegel97a
|texte= Study of the Semantics of ``Real'' Parallel Languages in TLA
}}
| This area was generated with Dilib version V0.6.33. |  |