Modelling SystemC scheduler by refinement
Identifieur interne : 005C91 ( Main/Exploration ); précédent : 005C90; suivant : 005C92Modelling SystemC scheduler by refinement
Auteurs : Dominique Cansell [France] ; Dominique Méry [France] ; Cyril ProchSource :
English descriptors
Abstract
Systems on Chip, or shortly SoCs, and SoC architectures denote a challenging set of problems of specification, modelling techniques, security issues and structuring questions. Our methodology, for designing models of (SoC) system from requirements, leads to formally justify hints on the future architectural choices of that system ; it is based on the B event-based method, which integrates the incremental development of models using a theorem prover to validate each step of development called refinement. The target system is generally expressed using a programming language notation like SystemC ; the SystemC language is used by electronic designers to describe different parts of the system (hardware and software) ; SystemC constitutes a general framework for simulating and validating the design of the system under construction. The semantics of SystemC is based on its scheduling algorithm described in the language reference manual and we develop a B model of the scheduling. The B \textit{scheduling} model left unspecified parameters depending on the simulated SystemC program and those parameters are instantiated from the operational semantics of the developed SystemC program. By instantiation, we obtain a B abstract model of the simulated program and we can study properties of the SystemC program by simulation. B models are completely validated by the proof assistant of the event-B method. Finally, our models provide a sound framework for understanding the scheduling process.
Affiliations:
- France
- Grand Est, Lorraine (région)
- Nancy
- Centre national de la recherche scientifique, Institut national de recherche en informatique et en automatique, Laboratoire lorrain de recherche en informatique et ses applications, Mosel (Loria), Université de Lorraine
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 004292
- to stream Crin, to step Curation: 004292
- to stream Crin, to step Checkpoint: 000139
- to stream Main, to step Merge: 005F14
- to stream Main, to step Curation: 005C91
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="73">Modelling SystemC scheduler by refinement</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:cansell05b</idno>
<date when="2005" year="2005">2005</date>
<idno type="wicri:Area/Crin/Corpus">004292</idno>
<idno type="wicri:Area/Crin/Curation">004292</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">004292</idno>
<idno type="wicri:Area/Crin/Checkpoint">000139</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000139</idno>
<idno type="wicri:Area/Main/Merge">005F14</idno>
<idno type="wicri:Area/Main/Curation">005C91</idno>
<idno type="wicri:Area/Main/Exploration">005C91</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Modelling SystemC scheduler by refinement</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Proch, Cyril" sort="Proch, Cyril" uniqKey="Proch C" first="Cyril" last="Proch">Cyril Proch</name>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Event B method - refinement - scheduler - operational semantics - systemC</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en" wicri:score="2822">Systems on Chip, or shortly SoCs, and SoC architectures denote a challenging set of problems of specification, modelling techniques, security issues and structuring questions. Our methodology, for designing models of (SoC) system from requirements, leads to formally justify hints on the future architectural choices of that system ; it is based on the B event-based method, which integrates the incremental development of models using a theorem prover to validate each step of development called refinement. The target system is generally expressed using a programming language notation like SystemC ; the SystemC language is used by electronic designers to describe different parts of the system (hardware and software) ; SystemC constitutes a general framework for simulating and validating the design of the system under construction. The semantics of SystemC is based on its scheduling algorithm described in the language reference manual and we develop a B model of the scheduling. The B \textit{scheduling} model left unspecified parameters depending on the simulated SystemC program and those parameters are instantiated from the operational semantics of the developed SystemC program. By instantiation, we obtain a B abstract model of the simulated program and we can study properties of the SystemC program by simulation. B models are completely validated by the proof assistant of the event-B method. Finally, our models provide a sound framework for understanding the scheduling process.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Nancy</li>
</settlement>
<orgName><li>Centre national de la recherche scientifique</li>
<li>Institut national de recherche en informatique et en automatique</li>
<li>Laboratoire lorrain de recherche en informatique et ses applications</li>
<li>Mosel (Loria)</li>
<li>Université de Lorraine</li>
</orgName>
</list>
<tree><noCountry><name sortKey="Proch, Cyril" sort="Proch, Cyril" uniqKey="Proch C" first="Cyril" last="Proch">Cyril Proch</name>
</noCountry>
<country name="France"><region name="Grand Est"><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
</region>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005C91 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005C91 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Exploration |type= RBID |clé= CRIN:cansell05b |texte= Modelling SystemC scheduler by refinement }}
This area was generated with Dilib version V0.6.33. |