Modelling SystemC scheduler by refinement

Dominique Cansell 1 Dominique Méry 1 Cyril Proch 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000564
Contributor : Cyril Proch <>
Submitted on : Thursday, November 3, 2005 - 9:15:13 AM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM
Long-term archiving on : Friday, April 2, 2010 - 6:21:04 PM

Identifiers

  • HAL Id : inria-00000564, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

318

Files downloads

374