ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Autres revues >>

L'Objet

1262-1137
logiciel, bases de données, réseaux
Publication abandonné
 

 ARTICLE VOL 14/4 - 2008  - pp.43-72  - doi:10.3166/obj.14.4.43-72
TITRE
Spécification et vérification d'un ordonnanceur en B via les automates temporisés

RÉSUMÉ
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.


ABSTRACT
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.


AUTEUR(S)
Odile NASR, Miloud RACHED, Jean-Paul BODEVEIX, Mamoun FILALI

MOTS-CLÉS
spécification, vérification, méthode B, raffinement, automates temporisés, ordonnancement temps-réel.

KEYWORDS
specification, verification, B method, refinement, timed automata, real time scheduling.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 34.95 €
• Non abonné : 34.95 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (360 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
made by WAW Lavoisier