Abstract
A formal framework is proposed for the verification of complex realtime systems, modeled as client-server scheduling systems, using the popular model-checking approach. Model-checking is often restricted by the large statespace of complex real-time systems. The scheduling of tasks in such systems can be taken advantage of for model-checking. Our implementation and experiments corroborate the feasibility of such an approach. Wide-applicability, significant state-space reduction, and several scheduling semantics are some of the important features in our theory and implementation.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, C. Courcoubetis, and D. L. Dill, “Model checking for real-time systems,” 5th IEEE LICS, 1990.
E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic verification of finite state concurrent system using temporal logic,” Procs. Workshop on Logics of Programs, Lecture Notes in Computer Science, vol. 131, pp. 52–71, 1981.
E. A. Emerson, “Temporal and Modal Logic,” in Handbook of Theoretical Computer Science, Ed. J. van Leeuwen, Elsevier Science Publishers B.V., 1990.
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi, “HyTech: the next generation,” Procs. IEEE Real-Time Systems Symposium, pp. 56–65, 1995.
M. G. Harbour, M. H. Klein, J. P. Lehoczky, “Fixed priority scheduling of periodic tasks with varying execution priority,” Procs. IEEE Real-Time System Symposium, pp. 116–128, 1991.
M. G. Harbour, M. H. Klein, J. P. Lehoczky, “Timing analysis for fixed-priority scheduling of hard real-time systems,” IEEE Trans. Software Engineering, vol. 20, no. 1, Jan. 1994.
D. I. Katcher, H. Arakawa, and J. K. Strosnider, “Engineering and analysis of fixed priority schedulers,” IEEE Trans. Software Engineering, vol. 19, pp. 920–934, Sept. 1993.
L. Lamport, “A Fast Mutual Exclusion Algorithm,” ACM Trans. on Computer Systems, vol. 5, no. 1, pp. 1–11, Feb. 1987.
J. P. Lehoczky, “Fixed priority scheduling of periodic task sets with arbitrary deadlines,” Procs. IEEE Real-Time Systems Symposium, pp. 201–209, 1990.
C. L. Liu and J. W. Layland, “Scheduling algorithms for multiprogramming in a hard-real-time environment,” Journal of the Association for Computing Machinery, vol. 20, no. 1, pp. 46–61, Jan. 1973.
J. P. Lehoczky, L. Sha, and Y. Ding, “The rate monotonic scheduling algorithm: exact characterization and average case behavior,” Procs. IEEE Real-Time Systems Symposium, pp. 166–171, 1989.
L. Sha and J. B. Goodenough, “Real-time scheduling theory and Ada,” IEEE Computer, vol. 23, pp. 53–62, Apr. 1990.
L. Sha, M. H. Klein, and J. B. Goodenough, “Rate monotonic analysis for real-time systems,” Foundations of Real-Time Computing: Scheduling and Resource Management, A. van Tilborg and G. M. Koob, Eds. New York: Kluwer, pp. 129–155, 1991.
K. W. Tindell, A. Burns, and A. J. Wellings, “Mode changes in priority pre-emptively scheduled systems,” Procs. IEEE Real-Time Systems Symposium, pp. 100–109, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hsiung, PA., Wang, F., Kuo, YS. (1999). Scheduling System Verification. In: Cleaveland, W.R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1999. Lecture Notes in Computer Science, vol 1579. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49059-0_2
Download citation
DOI: https://doi.org/10.1007/3-540-49059-0_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65703-3
Online ISBN: 978-3-540-49059-3
eBook Packages: Springer Book Archive