Modelling SystemC scheduler by refinement - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2005

Modelling SystemC scheduler by refinement

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.
Fichier principal
Vignette du fichier
cansellmeryprochisola2005.pdf (186.01 Ko) Télécharger le fichier
Loading...

Dates and versions

inria-00000564 , version 1 (03-11-2005)

Identifiers

  • HAL Id : inria-00000564 , version 1

Cite

Dominique Cansell, Dominique Méry, Cyril Proch. Modelling SystemC scheduler by refinement. IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation - ISOLA'05, Sep 2005, Columbia/USA. ⟨inria-00000564⟩
159 View
309 Download

Share

Gmail Facebook X LinkedIn More