Filali, Mamoun and Zaidi, Nabil Johnson's procedure: mechanization and parallelization. (2016) In: 7th International Real-Time Scheduling Open Problems Seminar (RTSOPS 2016) in conjunction with the 28th Euromicro Conference on Real-Time Systems : ECRTS 2016, 5 July 2016 - 5 July 2016 (Toulouse, France).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 84kB |
Abstract
In this note, we present a mechanization of Johnson’s procedure. We first specify the scheduling problem, we are concerned with. Then, we formalize Johnson’s procedure and prove an invariant. Thanks to this invariant, we prove the correctness of Johnson’s procedure and its optimality. Last, also thanks to the invariant, we elaborate a concurrent version of Johnson’s procedure which is correct by construction. We use the Python language for expression and experimentation purposes. The Isabelle HOL assistant theorem prover is used for validating the correctness.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| HAL Id: | hal-01517378 |
| Audience (conference): | International conference proceedings |
| Uncontrolled Keywords: | |
| Institution: | French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE) Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) Other partners > Lycée Blaise Pascal de Clermont-Ferrand (FRANCE) |
| Laboratory name: | |
| Statistics: | download |
| Deposited On: | 19 Apr 2017 11:54 |
Repository Staff Only: item control page
