Spécification et vérification d'un ordonnanceur en B via les automates temporisés

Autor:	Odile Nasr, Jean-Paul Bodeveix, Miloud Rached, Mamoun Filali
Rok vydání:	2008
Předmět:	Object-oriented programming Computer science Programming language B-Method Timed automaton Formal methods computer.software_genre Algorithm Real-time operating system computer Abstract machine Scheduling (computing)
Zdroj:	L'objet. 14:43-72
ISSN:	1262-1137
DOI:	10.3166/obj.14.4.43-72
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::c8d42227d44796fcfc4de0c2f0ff0dea https://doi.org/10.3166/obj.14.4.43-72 Zobrazit plný text záznamu