Abstract
The description of concurrent systems as a network of interacting processes helps to reduce the complexity of the specification. The same principle applies for the description of cyber-physical systems as a network of interacting components. We introduce a transition system based specification of cyber-physical components whose semantics is compositional with respect to a family of algebraic products. We give sufficient conditions for execution of a product of cyber-physical components to be correctly implemented by a lazy runtime expansion of the product construction. Our transition system algebra is implemented in the Maude rewriting logic system. As an example, we show that, under a coordination protocol, a set of autonomous energy-aware robots can self-sort themselves on a shared physical grid.
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
Notes
- 1.
We refer to [6] for a more detailed description of the Maude framework.
References
Arbab, F., Rutten, J.J.M.M.: A coinductive calculus of component connectors. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2002. LNCS, vol. 2755, pp. 34–55. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-40020-2_2. ISBN 978-3-540-20537-1
Baeten, J.C.M., Middelburg, C.A.: Real time process algebra with time-dependent conditions. J. Log. Algebraic Methods Program. 48(12), 1–38 (2001). https://doi.org/10.1016/S1567-8326(01)00004-2
Baier, C., et al.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61(2), 75–113 (2006). https://doi.org/10.1016/j.scico.2005.10.008. ISSN 0167–6423
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1), 109–137 (1984). https://doi.org/10.1016/S0019-9958(84)80025-X. ISSN 0019–9958
Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1
David, A., et al.: Timed I/O automata: a complete specification theory for real-time systems. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, 12–15 April 2010, pp. 91–100. ACM (2010). https://doi.org/10.1145/1755952.1755967
José Luiz Fiadeiro and Antónia Lopes: Heterogeneous and asynchronous networks of timed systems. Theor. Comput. Sci. 663, 1–33 (2017). https://doi.org/10.1016/j.tcs.2016.12.014
Fokkink, W.J.: Introduction to Process Algebra. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-662-04293-9. ISBN 978-3-540- 66579-3
van Hulst, A.C., Reniers, M.A., Fokkink, W.J.: Maximally permissive controlled system synthesis for non-determinism and modal logic. Disc. Event Dyn. Syst. 27(1), 109–142 (2016). https://doi.org/10.1007/s10626-016-0231-8
Kappé, T., et al.: Soft component automata: composition, compilation, logic, and verification. Sci. Comput. Program. 183, 102300 (2019). https://doi.org/10.1016/j.scico.2019.08.001
Kokash, N., Jaghoori, M.M., Arbab, F.: From timed reo networks to networks of timed automata. Electron. Notes Theor. Comput. Sci. 295, 11–29 (2013). https://doi.org/10.1016/j.entcs.2013.04.004. ISSN 1571–0661
Lafortune, S.: Discrete event systems: modeling, observation, and control. In: Annual Review of Control, Robotics, and Autonomous Systems, vol. 2, no. 1, pp. 141–159 (2019). https://doi.org/10.1146/annurev-control-053018-023659
Lion, B., Arbab, F., Talcott, C.: Runtime composition of systems of interacting cyber-physical components (2022)
Lion, B., Arbab, F., Talcott, C.L.: A rewriting framework for interacting cyber-physical agents. In: Margaria, T., Steffen, B (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, 22–30 October 2022, Proceedings, Part III. Lecture Notes in Computer Science, vol. 13703, pp. 356–375. Springer, Heidelberg (2022). https://doi.org/10.1007/978-3-031-19759-8_22
Lion, B., Arbab, F., Talcott, C.L.: A semantic model for interacting cyber-physical systems. In: Lange, J., et al. (eds.) Proceedings 14th Interaction and Concurrency Experience, ICE 2021, Online, 18 June 2021, vol. 347, pp. 77–95. EPTCS (2021). https://doi.org/10.4204/EPTCS.347.5
Mohajerani, S., Malik, R., Fabian, M.: A framework for compositional nonblocking verification of extended finite-state machines. Disc. Event Dyn. Syst. 26(1), 33–84 (2016). https://doi.org/10.1007/s10626-y015-0217-y
Sampath, M., Lafortune, S., Teneketzis, D.: Active diagnosis of discrete-event systems. IEEE Trans. Autom. Control 43(7), 908–929 (1998). https://doi.org/10.1109/9.701089
Talcott, C.: Cyber-physical systems and events. In: Wirsing, M., Banâtre, J.-P., Hölzl, M., Rauschmayer, A. (eds.) Software-Intensive Systems and New Computing Paradigms. LNCS, vol. 5380, pp. 101–115. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89437-7_6
Acknowledgement
Talcott was partially supported by the U. S. Office of Naval Research under award numbers N00014-15-1-2202 and N00014-20-1-2644, and NRL grant N0017317-1-G002. Arbab was partially supported by the U. S. Office of Naval Research under award number N00014-20-1-2644. We thank the reviewers for their critical comments and their helpful suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 Springer Nature Switzerland AG
About this paper
Cite this paper
Lion, B., Arbab, F., Talcott, C. (2023). Runtime Composition of Systems of Interacting Cyber-Physical Components. In: Madeira, A., Martins, M.A. (eds) Recent Trends in Algebraic Development Techniques. WADT 2022. Lecture Notes in Computer Science, vol 13710. Springer, Cham. https://doi.org/10.1007/978-3-031-43345-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-031-43345-0_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-43344-3
Online ISBN: 978-3-031-43345-0
eBook Packages: Computer ScienceComputer Science (R0)