On the modeling of sequential reactive systems by means of real time automata

E. M. Vinarskii ; V. A. Zakharov

Modelirovanie i analiz informacionnyh sistem, Tome 27 (2020) no. 4, pp. 396-411.

Résumé

Sequential reactive systems include hardware devices and software programs which operate in continuous interaction with the external environment, from which they receive streams of input signals (data, commands) and in response to them form streams of output signals. Systems of this type include controllers, network switches, program interpreters, system drivers. The behavior of some reactive systems is determined not only by the sequence of values of input signals, but also by the time of their arrival at the inputs of the system and the delays in computing the output signals. These aspects of reactive system computations are taken into account by real-time models of computation which include, in particular, realtime finite state machines (TFSMs). However, in most works where this class of real-time automata is studied a simple variant of TFSM semantics is used: the transduction relation computed by a TFSM is defined so that the elements of an output stream, regardless oftheir timestamps, follow in the same order as the corresponding elements ofthe input stream. This straightforward approach makes the model easier to analyze and manipulate, but it misses many important features of real-time computation. In this paper we study a more realistic semantics of TFSMs and show how to represent it by means of Labeled Transition Systems. The use of the new TFSM model also requires new approaches to the solution of verification problems in the framework of this model. For this purpose, we propose an alternative definition of TFSM computations by means of Labeled Transition Systems and show that the two definitions of semantics for the considered class of real-time finite state machines are in good agreement with each other. The use of TFSM semantics based on Labeled Transition Systems opens up the possibility of adapting well known real-time model checking techniques to the verification ofsequential reactive systems.

Détail

Keywords: reactive system, finite state machine, verification, security property, labeled transition system
Mots-clés : simulation.

Bibliographie

[1] A. Gill et al, Introduction to the theory of Finite-state Machines, 1962 | MR | Zbl

[2] A. Y. Savelev, Prikladnaya teoriya cifrovyh avtomatov, 1987 (In Russian)

[3] R. Alur, D. Dill, “A theory of timed automata”, Theoretical computer science, 126:2 (1994), 183–235 | DOI | MR | Zbl

[4] E. Asarin, P. Caspi, O. Maler, “Timed regular expressions”, Journal of the ACM, 49:2 (2001), 1–35 | MR

[5] E. Asarin, P. Caspi, O. Maler, “A Kleene theorem for timed automata”, Proceedings of 12-th Annual IEEE Symposium on Logic in Computer Science, LICS-97, IEEE, 1997, 160–171 | DOI

[6] R. Alur, P. Madhusudan, “Decision Problems for Timed Automata: A Survey, Formal Methods for the Design of Real-Time Systems”, Proceedings of the 4-th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-04, Springer, 2004, 1–24 | Zbl

[7] S. Lasota, I. Walukiewicz, “Alternating timed automata”, ACM Transactions on Computational Logic (TOCL), 9:2 (2008), 1–26 | DOI | MR

[8] M. Gromov, K. El-Fakih, N. Shabaldina, N. Yevtushenko, “Distinguing Non-deterministic Timed Finite State Machines”, Formal Techniques for Distributed Systems, Lecture Notes in Computer Science, 5522, Springer, 2009, 137–151 | DOI

[9] M. G. Merayo, M. Nunez, I. Rodriguez, “Formal testing from timed finite state machines”, Computer networks, 52:2 (2008), 432–460 | DOI | Zbl

[10] D. Bresolin, K. El-Fakih, T. Villa, N. Yevtushenko, “Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power”, Proceedings of the 5-th International Symposium on Games, Automata, Logics and Formal Verification, 2014, 203–216 | MR

[11] A. Tvardovskii, N. Yevtushenko, “Minimizing timed Finite State Machines”, Tomsk State University Journal of Control and Computer Science, 29:4 (2014), 77–83 | MR

[12] A. S. Tvardovskii, N. V. Yevtushenko, M. L. Gromov, “Minimizing finite state machines with time guards and timeouts”, Proceedings of the Institute for System Programming of the RAS, 29:4 (2017), 139–154 | DOI | MR

[13] A. S. Tvardovskii, N. V. Yevtushenko, “Deriving homing sequences for Finite State Machines with timed guards”, Sistemnaya informatika, 17 (2020), 1–10 | MR

[14] N. McKeown, T. Anderson, H. Balakrishnan, G. Parulkar, L. Peterson, J. Rexford, S. Shenker, J. Turner, “OpenFlow: enabling innovation in campus networks”, ACM SIGCOMM Computer Communication Review, 38:2 (2008), 69–74 | DOI

[15] E. Vinarskii, J. Lopez, N. Kushik, N. Yevtushenko, D. Zeghlache, “A Model Checking Based Approach for Detecting SDN Races”, Proceedings of the 31-st IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS, Springer, 2019, 194–211

[16] E. M. Vinarskii, V. A. Zakharov, “On the verification of strictly deterministic behavior of Timed Finite State Machines”, Proceedings of ISP RAS, 30:3 (2018), 325–340 | DOI

[17] C. Baier, J.-P. Katoen, Principles of model checking, MIT Press Cambridge, Cambridge, 2008 | MR | Zbl

[18] G. Behrmann, A. David, K. G. Larsen, “A tutorial on Uppaal”, Proceedings of the International School on Formal Methods for the Design of Computer, Communication, and Software Systems, Springer, 2004, 200–236 | Zbl