Spécification et vérification d'un ordonnanceur en B via les automates temporisés
Dans cet article, nous proposons une méthodologie permettant la spécification et la vérification des ordonnanceurs temps-réel. Elle est basée sur le mécanisme de raffinement de la méthode B. Nous introduisons progressivement les notions d'ordonnançabilité et du temps. Pour spécifier l'avancement du temps, nous utilisons les chronomètres, puis nous les raffinons par des horloges explicites. La machine B obtenue peut être considérée comme un automate temporisé qui raffine la spécification initiale.
This paper proposes a methodology for specifying and verifying real time schedulers using the B method. It is based on the refinement mechanism. We introduce successively the notions of scheduling and time. After having specified time management through stopwatches, a refinement introduces the notion of clocks. The obtained B machine can thus be considered as a timed automaton which refines the initial specification.
O.NASR, M.RACHED, J.BODEVEIX, M.FILALI
spécification, vérification, méthode B, raffinement, automates temporisés, ordonnancement temps-réel.
specification, verification, B method, refinement, timed automata, real time scheduling.
Français
|
