zbMATH — the first resource for mathematics

Schedulability of asynchronous real-time concurrent objects. (English) Zbl 1188.68085
Summary: We present a modular method for schedulability analysis of real time distributed systems. We extend the actor model, as the asynchronous model for concurrent objects, with real time using timed automata, and show how actors can be analyzed individually to make sure that no task misses its deadline. We introduce drivers to specify how an actor can be safely used. Using these drivers we can verify schedulability, for a given scheduler, by doing a reachability check with the Uppaal model checker. Our method makes it possible to put a finite bound on the process queue and still obtain schedulability results that hold for any queue length.

68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
68M14 Distributed systems
Full Text: DOI
[1] C. Hewitt, Procedural embedding of knowledge in planner, in: Proceedings of the Second International Joint Conference on Artificial Intelligence, 1971, pp. 167-184.
[2] G. Agha, The structure and semantics of actor languages, in: Proceedings of the REX Workshop, 1990, pp. 1-59.
[3] Alur, R.; Dill, D.L., A theory of timed automata, Theoretical comput. sci., 126, 2, 183-235, (1994) · Zbl 0803.68071
[4] Fersman, E.; Krcal, P.; Pettersson, P.; Yi, W., Task automata: schedulability, decidability and undecidability, Inform. and comput., 205, 8, 1149-1172, (2007) · Zbl 1121.68062
[5] Henzinger, T.A.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Inform. and comput., 111, 2, 193-244, (1994) · Zbl 0806.68080
[6] M. Bozga, S. Graf, I. Ober, I. Ober, J. Sifakis, The IF toolset, in: M. Bernardo, F. Corradini (Eds.), Formal Methods for the Design of Real-Time Systems, LNCS, vol. 3185, Springer, 2004, pp. 237-267. · Zbl 1105.68352
[7] Wang, F., Efficient verification of timed automata with BDD-like data structures, Sttt, 6, 1, 77-97, (2004)
[8] Tripakis, S.; Yovine, S.; Bouajjani, A., Checking timed Büchi automata emptiness efficiently, Formal methods syst. des., 26, 3, 267-292, (2005) · Zbl 1085.68083
[9] Larsen, K.G.; Pettersson, P.; Yi, W., UPPAAL in a nutshell, Sttt, 1, 1-2, 134-152, (1997) · Zbl 1060.68577
[10] Meyer, B., Eiffel: the language, (1992), Prentice-Hall, First printing: 1991 · Zbl 0779.68013
[11] L. de Alfaro, T.A. Henzinger, Interface automata, in: Proceedings of the ESEC/SIGSOFT FSE, 2001, pp. 109-120.
[12] Simons, D.P.L.; Stoelinga, M., Mechanical verification of the IEEE 1394a root contention protocol using uppaal2k, Sttt, 3, 4, 469-485, (2001) · Zbl 1053.68580
[13] Altisen, K.; Gößler, G.; Sifakis, J., Scheduler modeling based on the controller synthesis paradigm, Real-time syst., 23, 1-2, 55-84, (2002) · Zbl 1018.68006
[14] J.J.G. Garcia, J.C.P. Gutierrez, M.G. Harbour, Schedulability analysis of distributed hard real-time systems with multiple-event synchronization, in: Proceedings of the 12th Euromicro Conference on Real-Time Systems, IEEE, 2000, pp. 15-24.
[15] L. Nigro, F. Pupo, Schedulability analysis of real time actor systems using coloured petri nets, in: Proceedings of the Concurrent Object-Oriented Programming and Petri Nets, LNCS, vol. 2001, Springer, 2001, pp. 493-513. · Zbl 0976.68569
[16] E. Closse, M. Poize, J. Pulou, J. Sifakis, P. Venter, D. Weil, S. Yovine, TAXYS: a tool for the development and verification of real-time embedded systems, in: G. Berry, H. Comon, A. Finkel (Eds.), Proceedings of the Computer Aided Verification (CAV01), LNCS, vol. 2102, Springer, 2001, pp. 391-395. · Zbl 0991.68644
[17] C. Kloukinas, S. Yovine, Synthesis of safe, QoS extendible, application specific schedulers for heterogeneous real-time systems, in: Proceedings of the 15th Euromicro Conference on Real-Time Systems (ECRTS 2003), IEEE Computer Society, 2003, pp. 287-294.
[18] Liu, C.L.; Layland, J.W., Scheduling algorithms for multiprogramming in a hard real-time environment, J. ACM, 20, 1, 46-61, (1973) · Zbl 0265.68013
[19] Kupferman, O.; Vardi, M.Y.; Wolper, P., Module checking, Inform. and comput., 164, 2, 322-344, (2001) · Zbl 1003.68071
[20] Sirjani, M.; Movaghar, A.; Shali, A.; de Boer, F.S., Modeling and verification of reactive systems using rebeca, Fund. inform., 63, 4, 385-410, (2004) · Zbl 1082.68007
[21] Johnsen, E.B.; Owe, O., An asynchronous communication model for distributed concurrent objects, Software syst. model., 6, 1, 35-58, (2007)
[22] Courcoubetis, C.; Yannakakis, M., Minimum and maximum delay problems in real-time systems, Formal methods syst. des., 1, 4, 385-415, (1992) · Zbl 0777.68045
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.