Modelling SystemC scheduler by refinement
Identifieur interne : 004292 ( Crin/Corpus ); précédent : 004291; suivant : 004293Modelling SystemC scheduler by refinement
Auteurs : Dominique Cansell ; Dominique Méry ; 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.
Links to Exploration step
CRIN:cansell05bLe 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></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></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name></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><BibTex type="inproceedings"><ref>cansell05b</ref><crinnumber>A05-R-285</crinnumber><category>3</category><equipe>MOSEL</equipe><author><e>Cansell, Dominique</e><e>Méry, Dominique</e><e>Proch, Cyril</e></author><title>Modelling SystemC scheduler by refinement</title><booktitle>{IEEE Workshop on Leveraging Applications of Formal Methods, Verification, and Validation - ISOLA'05, Columbia, USA}</booktitle><year>2005</year><month>Sep</month><keywords><e>Event B method - refinement - scheduler - operational semantics - systemC</e></keywords><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.</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 004292 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 004292 | 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:cansell05b
|texte= Modelling SystemC scheduler by refinement
}}
| This area was generated with Dilib version V0.6.33. |  |