zbMATH — the first resource for mathematics

Compositional schedulability analysis of real-time actor-based systems. (English) Zbl 1371.68045
Summary: We present an extension of the actor model with real-time, including deadlines associated with messages, and explicit application-level scheduling policies, e.g.,“earliest deadline first” which can be associated with individual actors. Schedulability analysis in this setting amounts to checking whether, given a scheduling policy for each actor, every task is processed within its designated deadline. To check schedulability, we introduce a compositional automata-theoretic approach, based on maximal use of model checking combined with testing. Behavioral interfaces define what an actor expects from the environment, and the deadlines for messages given these assumptions. We use model checking to verify that actors match their behavioral interfaces. We extend timed automata refinement with the notion of deadlines and use it to define compatibility of actor environments with the behavioral interfaces. Model checking of compatibility is computationally hard, so we propose a special testing process. We show that the analyses are decidable and automate the process using the Uppaal model checker.
68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Aceto, L., Cimini, M., Ingólfsdóttir, A., Reynisson, A.H., Sigurdarson, S.H., Sirjani, M.: Modelling and simulation of asynchronous real-time systems using timed rebeca. In: Proceedings of Foundations of Coordination Languages and Software Architectures (FOCLASA’11), volume 58 of EPTCS, pp. 1-19 (2011)
[2] Acharya, A., Ranganathan, M., Saltz, J.H.: Sumatra: A language for resource-aware mobile programs. In: Mobile Object Systems, pp. 111-130 (1996) · Zbl 1060.68577
[3] Agha, G.: The structure and semantics of actor languages. In: Proceedings of the REX, Workshop, pp 1-59 (1990)
[4] Agha, G; Mason, I; Smith, S; Talcott, C, A foundation for actor computation, J. Funct. Program., 7, 1-72, (1997) · Zbl 0870.68091
[5] Aldrich, J., Sunshine, J., Saini, D., Sparks, Z.: Typestate-oriented programming. In: Proceedings of 24th ACM SIGPLAN conference companion on object oriented programming systems languages and applications, OOPSLA ’09, pp. 1015-1022 (2009) · Zbl 0870.68091
[6] Altisen, K; Gößler, G; Sifakis, J, Scheduler modeling based on the controller synthesis paradigm, Real-Time Syst., 23, 55-84, (2002) · Zbl 1018.68006
[7] Alur, R; Dill, DL, A theory of timed automata, Theoret. Comp. Sci., 126, 183-235, (1994) · Zbl 0803.68071
[8] Alur, R., Weiss, G.: Rtcomposer: a framework for real-time components with scheduling interfaces. In: de Alfaro, L., Palsberg, J. (eds.) Proceedings of Embedded software (EMSOFT’08), pp. 159-168. ACM (2008) · Zbl 1101.68694
[9] Armstrong, J, Erlang, Commun. ACM, 53, 68-75, (2010)
[10] Bérard, B; Petit, A; Diekert, V; Gastin, P, Characterization of the expressive power of silent transitions in timed automata, Fundam. Inf., 36, 145-182, (1998) · Zbl 0930.68077
[11] Berman, F., Wolski, R.: Scheduling from the perspective of the application. In: Proceedings of High Performance Distributed Computing (HPDC’96), pp. 100-111. IEEE Computer Society (1996) · Zbl 1188.68085
[12] Bertrand, N., Stainer, A., Jéron, T., Krichen, M.: A game approach to determinize timed automata. In: Proceedings of foundations of software science and computational structures, FOSSACS’11/ETAPS’11, pp. 245-259. Springer (2011) · Zbl 1326.68173
[13] Buttazzo, G.: Hard Real-Time Computing Systems, 3rd edn. Springer, Berlin (2011) · Zbl 1246.68001
[14] Cardell-Oliver, R., Glover, T.: A practical and complete algorithm for testing real-time systems. In: Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’98), volume 1486 of Lecture Notes in Computer Science, pp. 251-261 (1998) · Zbl 1003.68071
[15] Cattani, S; Kwiatkowska, MZ, A refinement-based process algebra for timed automata, Formal Asp. Comput., 17, 138-159, (2005) · Zbl 1101.68694
[16] Chang, P.-H., Agha, G.: Supporting reconfigurable object distribution for customized web applications. In: The 22nd Annual ACM Symposium on Applied Computing (SAC), pp. 1286-1292 (2007) · Zbl 1060.68577
[17] Chang, P.-H., Agha, G.: Towards context-aware web applications. In: 7th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS), pp. 239-252 (2007) · Zbl 1185.68401
[18] Cheong, E.: Actor-Oriented Programming for Wireless Sensor Networks. PhD thesis, Electrical Engineering and Computer Sciences University of California at Berkeley (2007) · Zbl 0806.68080
[19] Cheong, E., Lee, E.A., Zhao, Y.: Viptos: a graphical development and simulation environment for tinyos-based wireless sensor networks. In: Proceedings of Embedded net. sensor sys., SenSys 2005, pp. 302-302 (2005)
[20] Clarke, D., Lee, I.: Automatic test generation for the analysis of a real-time system: case study. In: IEEE Real Time Technology and Applications Symposium, pp. 112-124 (1997)
[21] Closse, E., Poize, M., Pulou, J., Sifakis, J., Venter, P., Weil, D., Yovine, S.: TAXYS: A tool for the development and verification of real-time embedded systems. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of Computer Aided Verification, volume 2102 of LNCS, pp. 391-395. Springer (2001) · Zbl 0991.68644
[22] Courcoubetis, C; Yannakakis, M, Minimum and maximum delay problems in real-time systems, Form. Methods Syst. Des., 1, 385-415, (1992) · Zbl 0777.68045
[23] David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: Proceedings of Hybrid Systems: Computation and Control (HSCC’10), pp. 91-100. ACM (2010) · Zbl 1361.68143
[24] de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Timed interfaces. In: Proceedings of Embedded Software (EMSOFT), volume 2491 of LNCS, pp. 108-122 (2002) · Zbl 1027.68785
[25] Fersman, E; Krcal, P; Pettersson, P; Yi, W, Task automata: schedulability, decidability and undecidability, Inf. Comput., 205, 1149-1172, (2007) · Zbl 1121.68062
[26] Finkel, O.: Undecidable problems about timed automata. In: Asarin, E., Bouyer, P. (eds.) Proceedings of Formal Modeling and Analysis of Timed Systems (FORMATS’06), volume 4202 of LNCS, pp. 187-199. Springer (2006) · Zbl 1141.68433
[27] Garcia, J.J.G., Gutierrez, J.C.P., Harbour, M.G.: Schedulability analysis of distributed hard real-time systems with multiple-event synchronization. In: Proceedings of 12th Euromicro Conference on Real-Time Systems, pp. 15-24. IEEE (2000)
[28] Geilen, S., Tripakis, M., Wiggers, M.: The earlier the better: a theory of timed actor interfaces. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) Proceedings of Hybrid Systems: Computation and Control (HSCC’11), pp. 23-32. ACM (2011) · Zbl 1362.68049
[29] Grabe, I., Jaghoori, M.M., Klein, J., Klüppelholz, S., Stam, A., Baier, C., Blechmann, T., Aichernig, B.K., de Boer, F.S., Griesmayer, A., Johnsen, E.B., Kyas, M., Leister, W., Schlatte, R., Steffen, M., Tschirner, S., Liang, X., Yi, W.: The credo methodology - (extended version). In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) Proceedings of 8th Formal Methods for Components and Objects (FMCO’09), volume 6286 of LNCS, pp. 41-69 (2009) · Zbl 1162.68396
[30] Haller, P; Odersky, M, Scala actors: unifying thread-based and event-based programming, Theor. Comput. Sci., 410, 202-220, (2009) · Zbl 1162.68396
[31] Henzinger, TA; Nicollin, X; Sifakis, J; Yovine, S, Symbolic model checking for real-time systems, Inf. Comput., 111, 193-244, (1994) · Zbl 0806.68080
[32] Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using uppaal. In: Formal Methods and Testing, volume 4949 of LNCS, pp. 77-117 (2008)
[33] Hewitt, C.: Procedural embedding of knowledge in planner. In: Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pp. 167-184 (1971)
[34] Hewitt, C.: What is commitment? physical, organizational, and social (revised). In: Proceedings of Coordination, Organizations, Institutions, and Norms in Agent Systems II, LNCS Series, pp. 293-307. Springer (2007)
[35] Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. In Proc. Arch. Support for Prog. Lang. and Operating Sys., pages 93-104, (2000) · Zbl 1101.68694
[36] Jaghoori, M.M.: Composing real-time concurrent objects—refinement, compatibility and schedulability. In: Proceedings of Fundamentals of Software Engineering (FSEN’11), volume 7141 of LNCS, pp. 96-111. Springer (2011) · Zbl 1353.68207
[37] Jaghoori, M.M.: From nonpreemptive to preemptive scheduling: from single-processor to multi-processor. In: Chu, W.C., Wong, W.E., Palakal, M.J., Hung, C.-C. (eds.) Proceedings of ACM Symposium on Applied Computing (SAC’11), pp. 717-722. ACM (2011) · Zbl 1018.68006
[38] Jaghoori, MM; Boer, FS; Chothia, T; Sirjani, M, Schedulability of asynchronous real-time concurrent objects, J. Logic Alg. Prog., 78, 402-416, (2009) · Zbl 1188.68085
[39] Jaghoori, M.M., Hlynsson, Ó., Sirjani, M.: Networks of real-time actors. In: Arbab, F., Ölveczky, P.C. (eds.) Formal Aspects of Component Software - 8th International Symposium (FACS’11), volume 7253 of LNCS, pp. 168-186. Springer (2012)
[40] Jaghoori, M.M., Longuet, D., de Boer, F.S., Chothia, T.: Schedulability and compatibility of real time asynchronous objects. In: Proceedings of Real Time Systems Symposium, pp. 70-79. IEEE CS (2008)
[41] Jard, C., Jéron, T., Morel, P.: Verification of test suites. In: International Conference on Testing Communicating Systems (TestCom 2000), pp. 3-18 (2000) · Zbl 0777.68045
[42] Johnsen, EB; Owe, O, An asynchronous communication model for distributed concurrent objects, Softw. Syst. Model., 6, 35-58, (2007)
[43] Karmani, R.K., Shali, A., Agha, G.: Actor frameworks for the jvm platform: a comparative analysis. In: Proceedings of Principles and Practice of Progress in Java (PPPJ’09), pp. 11-20. ACM (2009) · Zbl 1121.68062
[44] Khoumsi, A., Jéron, T., Marchand, H.: Test cases generation for nondeterministic real-time systems. In: Formal Approaches to Software Testing (FATES’03), volume 2931 of LNCS, pp. 131-146 (2004) · Zbl 1185.68415
[45] Kloukinas, C., Yovine, S.: Synthesis of safe, QoS extendible, application specific schedulers for heterogeneous real-time systems. In: Proceedings of Euromicro Conference on Real-Time Systems, pp. 287-294. IEEE CS (2003) · Zbl 1188.68085
[46] Krichen, M., Tripakis, S.: Black-box conformance testing for real-time systems. In: Model Checking Software, 11th International SPIN Workshop, volume 2989 of LNCS, pp. 109-126 (2004) · Zbl 1125.68370
[47] Krichen, M; Tripakis, S, Conformance testing for real-time systems, Form. Methods Syst. Des., 34, 238-304, (2009) · Zbl 1180.68072
[48] Kupferman, O; Vardi, MY; Wolper, P, Module checking, Inf. Comput., 164, 322-344, (2001) · Zbl 1003.68071
[49] Larsen, KG; Pettersson, P; Yi, W, UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transf. (STTT), 1, 134-152, (1997) · Zbl 1060.68577
[50] Lee, E.A., Liu, X., Neuendorffer, S.: Classes and inheritance in actor-oriented design. ACM Trans. Embedded Comput. Syst. 8(4), (2009) · Zbl 0870.68091
[51] Lee, EA; Neuendorffer, S; Wirthlin, MJ, Actor-oriented design of embedded hardware and software systems, J. Circuits Syst. Comput., 12, 231-260, (2003)
[52] MacKenzie, K., Wolverson, N.: Camelot and grail: resource-aware functional programming for the jvm. In: Trends in Functional Programming, pp. 29-46 (2003)
[53] Meyer, B.: Eiffel: The Language. Prentice-Hall, New Jersey, 1992. (first printing: 1991) · Zbl 0779.68013
[54] Moreau, L; Queinnec, C, Resource aware programming, ACM Trans. Program. Lang. Syst., 27, 441-476, (2005)
[55] Nielsen, B., Skou, A.: Automated test generation from timed automata. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), volume 2031 of LNCS, pp. 343-357 (2001) · Zbl 0978.68538
[56] Nigro, L., Pupo, F.: Schedulability analysis of real time actor systems using coloured petri nets. In: Proceedings of Concurrent Object-Oriented Prog. and Petri Nets, volume 2001 of LNCS, pp. 493-513. Springer (2001) · Zbl 0976.68569
[57] Nobakht, B., de Boer, F.S., Jaghoori, M.M., Schlatte, R.: Programming and deployment of active objects with application-level scheduling. In: Proceedings of ACM Symposium on Applied Computing (SAC’12). ACM (2012). To appear
[58] Rajamani, S., Rehof, J.: A behavioral module system for the pi-calculus. In: Cousot, P. (ed.) Static Analysis Symposium. LNCS, vol. 2126, pp. 375-394. Springer, Berlin (2001) · Zbl 0997.68514
[59] Reed, G; Roscoe, A, The timed failures - stability model for CSP, Theor. Comput. Sci., 211, 85-127, (1999) · Zbl 0912.68038
[60] Schmaltz, J., Tretmans, J.: On conformance testing for timed systems. In: Formal Modeling and Analysis of Timed Systems, volume 5215 of LNCS, pp. 250-264. Springer (2008) · Zbl 1171.68556
[61] Shin, I; Lee, I, Compositional real-time scheduling framework with periodic model, ACM Trans. Embed. Comput. Syst., 7, 30:1-30:39, (2008)
[62] Simons, DPL; Stoelinga, M, Mechanical verification of the IEEE 1394a root contention protocol using uppaal2k, Int. J. Softw. Tools Technol. Transf. (STTT), 3, 469-485, (2001) · Zbl 1053.68580
[63] Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, volume 7000 of LNCS, pp. 20-56. Springer (2011)
[64] Tretmans, J, Test generation with inputs, outputs and repetitive quiescence, Softw. Conc. Tools, 17, 103-120, (1996) · Zbl 0858.68061
[65] Tripakis, S.: Verifying progress in timed systems. In: Katoen, J-P. (ed.) Formal Methods for Real-Time and Probabilistic Systems. LNCS, vol. 1601, pp. 299-314. Springer, Berlin, Heidelberg (1999). doi:10.1007/3-540-48778-6_18
[66] Tripakis, S, Folk theorems on the determinization and minimization of timed automata, Inf. Process. Lett., 99, 222-226, (2006) · Zbl 1185.68401
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.