Abstract
We present a simple but elegant prototyping language for describing real-time systems including specific features as timeouts, explicit locations, timed migration and timed communication. The parallel execution of a step is provided by multiset labelled transitions. In order to illustrate its features, we describe a railway control system. Moreover, we define some behavioural equivalences matching multisets of actions that could happen in a given range of time (up to a timeout). We define the strong time-bounded bisimulation and the strong open time-bounded bisimulation, and prove that the latter one is a congruence. By using various bisimulations over the behaviours of real-time systems, we can check which behaviours are closer to an optimal and safe behaviour.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Aman, B., Ciobanu, G.: Real-Time Migration Properties of rTiMo Verified in Uppaal. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 31–45. Springer, Heidelberg (2013)
Aman, B., Ciobanu, G., Koutny, M.: Behavioural Equivalences over Migrating Processes with Timers. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 52–66. Springer, Heidelberg (2012)
Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. In: Monographs in Theoretical Computer Science, An EATCS Series. Springer, Berlin (2002)
Ciobanu, G.: Behaviour Equivalences in Timed Distributed π-Calculus. In: Wirsing, M., Banâtre, J.-P., Hölzl, M., Rauschmayer, A. (eds.) Software Intensive Systems. LNCS, vol. 5380, pp. 190–208. Springer, Heidelberg (2008)
Ciobanu, G., Juravle, C.: Flexible Software Architecture and Language for Mobile Agents. Concurrency and Computation: Practice and Experience 24, 559–571 (2012)
Ciobanu, G., Koutny, M.: Modelling and Verification of Timed Interaction and Migration. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 215–229. Springer, Heidelberg (2008)
Ciobanu, G., Koutny, M.: Timed Migration and Interaction With Access Permissions. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 293–307. Springer, Heidelberg (2011)
Ciobanu, G., Prisacariu, C.: Timers for Distributed Systems. Electronic Notes in Theoretic Computer Science 164(3), 81–99 (2006)
Ciobanu, G., Zheng, M.: Automatic Analysis of TiMo Systems in PAT. In: Proc. 18th International Conference on Engineering of Complex Computer Systems, pp. 121–124. IEEE Computer Society (2013)
Han, T., Katoen, J.-P., Mereacre, A.: Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 244–258. Springer, Heidelberg (2008)
Heitmeyer, C., Lynch, N.: The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems. In: Proc. of IEEE Real-Time Systems Symposium, pp. 120–131 (1994)
Kamide, N.: Bounded Linear-Time Temporal Logic: A Proof-Theoretic Investigation. Annals of Pure and Applied Logic 163, 439–466 (2012)
Larsen, K.G., Petterson, P., Yi, W.: Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer 1(2), 134–152 (1997)
Milner, R.: Communicating and Mobile Systems: the π-calculus. Cambridge University Press (1999)
Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)
Yi, W., Pettersson, P., Daniels, M.: Automatic Verification of Real-time Communicating Systems by Constraint-Solving. In: International Conference on Formal Description Techniques, pp. 223–238 (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Aman, B., Ciobanu, G. (2015). Timed Mobility and Timed Communication for Critical Systems. In: Núñez, M., Güdemann, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2015. Lecture Notes in Computer Science(), vol 9128. Springer, Cham. https://doi.org/10.1007/978-3-319-19458-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-19458-5_10
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19457-8
Online ISBN: 978-3-319-19458-5
eBook Packages: Computer ScienceComputer Science (R0)