Abstract
We propose a compositional approach for the Partial Order Reduction (POR) in the state space generation of asynchronous timed actors. We define the concept of independent actors as the actors that do not send messages to a common actor. The approach avoids exploring unnecessary interleaving of executions of independent actors. It performs on a component-based model where actors from different components, except for the actors on borders, are independent. To alleviate the effect of the cross-border messages, we enforce a delay condition, ensuring that an actor introduces a delay in its execution before sending a message across the border of its component. Within each time unit, our technique generates the state space of each individual component by taking its received messages into account. It then composes the state spaces of all components. We prove that our POR approach preserves the properties defined on timed states (states where the only outgoing transition shows the progress of time). We generate the state space of a case study in the domain of air traffic control systems based on the proposed POR. The results on our benchmarks illustrate that our POR method, on average, reduces the time and memory consumption by 76 and 34%, respectively.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, USA (1986)
Akka library (2021). http://akka.io
Bagheri, M., Sirjani, M., Khamespanah, E., Baier, C., Movaghar, A.: Magnifier: a compositional analysis approach for autonomous traffic control. IEEE Trans. Softw. Eng. 1 (2021). https://doi.org/10.1109/TSE.2021.3069192
Bagheri, M., et al.: Coordinated actors for reliable self-adaptive systems. In: Kouchnarenko, O., Khosravi, R. (eds.) FACS 2016. LNCS, vol. 10231, pp. 241–259. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57666-4_15
Bagheri, M., et al.: Coordinated actor model of self-adaptive track-based traffic control systems. J. Syst. Softw. 143, 116–139 (2018)
Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055643
Boer, F.D., et al.: A survey of active object languages. ACM Comput. Surv. 50(5) (2017). https://doi.org/10.1145/3122848
Earle, C.B., Fredlund, L.Å.: Verification of timed erlang programs using McErlang. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE -2012. LNCS, vol. 7273, pp. 251–267. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30793-5_16
Eckhardt, J., Mühlbauer, T., Meseguer, J., Wirsing, M.: Statistical model checking for composite actor systems. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 143–160. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37635-1_9
Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176–185. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0023731
Håkansson, J., Pettersson, P.: Partial order reduction for verification of real-time components. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 211–226. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75454-1_16
Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2), 202–220 (2009). distributed Computing Techniques
Hansen, H., Lin, S.-W., Liu, Y., Nguyen, T.K., Sun, J.: Diamonds are a girl’s best friend: partial order reduction for timed automata with abstractions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 391–406. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_26
Hewitt, C.: Description and theoretical analysis (using schemata) of planner: A language for proving theorems and manipulating models in a robot. Technical report, Massachusetts Inst of Tech Cambridge ArtificiaL Intelligence Lab (1972)
Khamespanah, E., Sirjani, M., Sabahi Kaviani, Z., Khosravi, R., Izadi, M.J.: Timed rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Sci. Comput. Program. 98, 184–204 (2015). special Issue on Programming Based on Actors, Agents and Decentralized Control
Lohstroh, M., et al.: Reactors: a deterministic model for composable reactive systems. In: Chamberlain, R., Edin Grimheden, M., Taha, W. (eds.) CyPhy/WESE -2019. LNCS, vol. 11971, pp. 59–85. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-41131-2_4
Minea, M.: Partial order reduction for model checking of timed automata. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 431–446. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48320-9_30
Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56922-7_34
Source codes (2021). https://github.com/maryambagheri1989/POR/
Ptolemaeus, C.: System Design, Modeling, and Simulation: Using Ptolemy II. Ptolemy.org, Berkeley, CA, USA (2014)
Afra Tool (2021). http://rebeca-lang.org/alltools/Afra
Reynisson, A.H., et al.: Modelling and simulation of asynchronous real-time systems using timed rebeca. Sci. Comput. Program. 89, 41–68 (2014). https://doi.org/10.1016/j.scico.2014.01.008, http://www.sciencedirect.com/science/article/pii/S0167642314000239, special issue on the 10th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2011)
Sirjani, M., Lee, E.A., Khamespanah, E.: Model checking software in cyberphysical systems. In: 2020 IEEE 44th Annual Computers, Software, and Applications Conference (COMPSAC), pp. 1017–1026 (2020)
Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using rebeca. Fundam. Inf. 63(4), 385–410 (2004)
Tan, T.H., Liu, Y., Sun, J., Dong, J.S.: Verification of orchestration systems using compositional partial order reduction. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 98–114. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24559-6_9
Virding, R., Wikström, C., Williams, M., Armstrong, J.: Concurrent Programming in ERLANG, 2nd (ed.). Prentice Hall International (UK) Ltd., GBR, London (1996)
Ölveczky, P.C., Meseguer, J.: Real-time maude 2.1. Electron. Notes Theor. Comput. Sci. 117, 285–314 (2005). proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Bagheri, M., Sirjani, M., Khamespanah, E., Hojjat, H., Movaghar, A. (2022). Partial Order Reduction for Timed Actors. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds) Software Verification. NSV VSTTE 2021 2021. Lecture Notes in Computer Science(), vol 13124. Springer, Cham. https://doi.org/10.1007/978-3-030-95561-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-95561-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-95560-1
Online ISBN: 978-3-030-95561-8
eBook Packages: Computer ScienceComputer Science (R0)