M.R. Mousavi, M.A. Reniers, T. Basten, M.R.V. Chaudron, Proceedings of First International Workshop on Formal Modeling and Analysis of Timed Systems ( FORMATS'03), Marseille, France, September 2003, volume 2791 of Lecture Notes in Computer Science, pp. 134-150, Springer-Verlag, May 2004.
In this paper, we introduce a dense time process algebraic formalism with support for specification of (shared) resource requirements and resource schedulers. The goal of this approach is to facilitate and formalize introduction of scheduling concepts into process algebraic specification using separate specifications for resource requiring processes, schedulers and systems composing the two. The benefits of this research are twofold. Firstly, it allows for formal investigation of scheduling strategies. Secondly, it provides the basis for an extension of schedulability analysis techniques to the formal verification process, facilitating the modeling of real-time systems in a process algebraic manner using the rich background of research in scheduling theory.
(Paper in .ps format in .pdf format) (Presentation in .pdf format)
@InProceedings{MousaviFormats03,
title = "{PARS}: A Process Algebra with Resource and Schedulers",
author = "Mousavi, MohammadReza and Reniers, Michel and Basten, Twan and Chaudron, Michel",
booktitle = "Proceedings of the First International Workshop on Formal Modeling and Analysis of Timed Systems (Formats'03)",
editor = "Larsen, Kim G. and Niebert, Peter",
series = "Lecture Notes in Computer Science",
volume = "2791",
pages = "134--150",
publisher = "Springer-Verlag, Berlin, Germany, May, 2004"
}
Back to Publications Page