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.
Abstract: The purpose of this paper is to present our timed B method for modelling real time reactive systems. It allows to specify and check functional and temporal properties of a system. In this method, we have extended the property and the substitution languages of classic B. In the former, we introduce a variant of a timed logic incorporating events and high level predicates. In the latter, we add a new substitution to express time progression.
