Hassan MOTALLEBI, Mohammad Abdollahi AZGOMI, Mohammad Saber MIRZAEI

A new extension of activity networks for modeling and verification of timed systems

Stochastic activity networks (SANs) are a well-known petri net-based formalism used for the performance and dependability modeling of a wide range of systems. On the other hand, the growing complexity of timed systems makes it imperative to apply formal analysis techniques in the early stages of the system's development. Finding a suitable framework for the modeling, evaluation, and verification of these systems is still a great challenge. In this paper, we introduce a new formalism named timed activity networks (TANs), which are based on the activity networks that are the nondeterministic settings of the SANs. The advantages of TANs are 2-fold: 1) allowing the construction of more compact petri net-based models of timed systems and 2) allowing the assignment of time intervals to timed activities where the activity completion rates are marking-dependent, which makes TANs a better model for timed systems. Thanks to the presence of the input/output gates, TANs are capable of describing a situation whose specification using petri net-based formalisms was not practical, due to the naivety of the enabling and firing rules in these models. In addition, a great benefit of TANs is the similarity of their primitives and notations to ordinary SANs, which allows us to easily obtaining these 2 models from each other. Accordingly, SANs can be used for performance, and dependability modeling and evaluation, while TANs can be used for the model checking of timed systems. In this paper, we present the definitions, semantics, and model checking techniques of the proposed formalism. In order to model check TAN models, a transformation procedure is given for translating TAN models into the equivalent linear hybrid automaton, which can then be used with the existing techniques and tools.

Anahtar Kelimeler:

Timed systems, modeling and verification, stochastic activity networks, timed activity networks, polyhedral computations

A new extension of activity networks for modeling and verification of timed systems

Keywords:

Timed systems, modeling and verification, stochastic activity networks, timed activity networks, polyhedral computations,

PDF

___

[1] A. Movaghar, “Stochastic activity networks: a new definition and some properties”, Scientia Iranica, Vol. 8, pp. 303–311, 2001.
[2] M. Uzam, A.H. Jones, “A new Petri-net–based synthesis technique for supervisory control of discrete event systems”, Turkish Journal of Electrical Engineering & Computer Sciences, Vol. 10, pp. 85–109, 2002.
[3] R. Samet, O.F. Duman, “Behaviors of real-time schedulers under resource modification and a steady scheme with bounded utilization”, Turkish Journal of Electrical Engineering & Computer Sciences, Vol. 18, pp. 1115–1130, 2010.
[4] R. Alur, D. Dill, “Automata for modelling real-time systems”, Lecture Notes in Computer Science, Vol. 443, pp. 322–335, 1990.
[5] G. Behrmann, J. Bengtsson, A. David, K. Larsen, P. Pettersson, W. Yi, “UPPAAL implementation secrets”, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, pp. 3–22, 2002.
[6] T.A. Henzinger, P. Ho, H. Wong-Toi, “HyTech: a model checker for hybrid systems”, Proceedings of the 6th International Conference on Computer Aided Verification, pp. 460–463, 1997.
[7] F. Laroussinie, K. Larsen, “CMC: a tool for compositional model-checking of real-time”, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification, pp. 439–456, 1998.
[8] M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, S. Yovine, “Kronos: A model-checking tool for real-time systems”, Proceedings of the 10th International Conference on Computer Aided Verification, pp. 546–550, 1998.
[9] J. Srba, “Comparing the expressiveness of timed automata and timed extensions of Petri nets”, Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems, pp. 15–32, 2008.
[10] T. Henzinger, “The theory of hybrid automata”, Proceedings of the 11th Annual Symposium on Logic in Computer Science, pp. 278–292, 1996.
[11] P. Merlin, “A study of recoverability of computing systems”, PhD Thesis, Department of Computer Science, University of California, Irvine, 1974.
[12] P. Merlin, D. Farber, “Recoverability of Communication protocols: implications of a theoretical study”, IEEE Transactions on Communications, Vol. 24, pp.1036–1043, 1976.
[13] B. B´erard, F. Cassez, S. Haddad, D. Lime, O. Roux, “Comparison of the expressiveness of timed automata and time Petri nets”, Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems, pp. 211–225, 2005.
[14] M. Abdollahi Azgomi, A. Movaghar, “A modelling tool for hierarchical stochastic activity networks”, Simulation Modelling Practice and Theory, Vol. 13, pp. 505–524, 2005.
[15] M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, G. Franceschinis, Modelling with Generalized Stochastic Petri Nets, New York, Wiley, 1995.
[16] A. Abbarin, M. Firuzabad, A. Ozdemir, “An extended component-based reliability model for protective systems ¨ to determine routine test schedule”, Turkish Journal of Electrical Engineering & Computer Sciences, Vol. 19, pp. 303–315, 2011.
[17] M. Cakiro˘glu, A. Ozcerit, “Design and evaluation of a query-based jamming detection algorithm for wireless sensor ¨ networks”, Turkish Journal of Electrical Engineering & Computer Sciences, Vol. 19, pp. 1–19, 2011.
[18] W.H. Sanders, W. Obal II, M. Qureshi, F. Widjanarko, “The UltraSAN modeling environment”, Performance Evaluation, Vol. 24, pp. 89–115, 1995.
[19] D.D. Deavours, G. Clark, T. Courtney, D. Daly, S. Derisavi, J. Doyle, W.H. Sanders, P. Webster, “The M¨obius framework and its implementation”, IEEE Transactions on Software Engineering, Vol. 28, pp. 956–969, 2002.
[20] A. Movaghar, J.F. Meyer, “Performability modeling with stochastic activity networks”, Proceedings of the 1984 Real-Time Systems Symposium, pp. 215–224, 1984.
[21] A. Movaghar, “Performability modeling with stochastic activity networks”, PhD Dissertation, Department of Electrical Engineering, University of Michigan, 1985.
[22] M. Abdollahi Azgomi, A. Movaghar, “An introduction to high-level stochastic activity networks” International Reviews on Computers and Software, Praise Worthy Prize, Vol. 1, pp. 20–30, 2006.
[23] M. Abdollahi Azgomi, A. Movaghar, “Modeling and evaluation with object stochastic activity networks”, Proceedings of the 1st International Conference on Quantitative Evaluation of Systems, pp. 326–327, 2004.
[24] W.H. Sanders, J.F. Meyer, “Stochastic activity networks: formal definitions and concepts”, Lecture Notes in Computer Science, Vol. 2090, pp. 315–343, 2001.
[25] M. Abdollahi Azgomi, A. Movaghar, “A modeling tool for a new definition of stochastic activity networks”, Iranian Journal of Science and Technology, Transaction B (Technology), Vol. 29, pp. 79–92, 2005.
[26] A. Khalili, A. Jalaly Bidgoly, M. Abdollahi Azgomi, “PDETool: a multi-formalism modeling tool for discrete-event systems based on SDES description”, Lecture Notes in Computer Science, Vol. 5606, pp. 343–352, 2009.
[27] D. Lime, O. Roux, “Formal verification of real-time systems with preemptive scheduling”, Real-Time Systems, Vol. 41, pp. 118–151, 2009.
[28] J. McManis, P. Varaiya, “Suspension automata: a decidable class of hybrid automata”, Proceedings of the 6th International Conference on Computer Aided Verification, pp. 105–117, 1994.
[29] E. Fersman, P. Krc´al, P. Pettersson, W. Yi, “Task automata: schedulability, decidability and undecidability”, Information and Computation, Vol. 205, pp. 1149–1172, 2007.
[30] O. Roux, D. Lime, “Time Petri nets with inhibitor hyperarcs: formal semantics and state space computation”, Proceedings of the 25th International Conference on Applications and Theory of Petri Nets, pp. 371–390, 2004.
[31] T. Henzinger, Z. Manna, A. Pnueli, “Timed transition systems”, Proceedings of the REX Workshop Real-Time: Theory in Practice, Lecture Notes in Computer Science, Vol. 600, pp. 226–251, 1992.
[32] D. Lime, O. Roux, “Model-checking of time Petri nets using the state class timed automaton”, Discrete Event Dynamic Systems, Vol. 16, pp. 179–205, 2006.
[33] R. Bagnara, P. Hill, E. Zaffanella, “The Parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems”, Science of Computer Programming, Vol. 72, pp. 3–21, 2008.
[34] R. Bagnara, P.M. Hill, E. Zaffanella, “The Parma polyhedra library user’s manual”, Department of Mathematics, University of Parma, Parma, Italy, Version 0.11.2, Available: http://www.cs.unipr.it/ppl/, 2011.
[35] F. Cassez, O. Roux, “Structural translation from time Petri nets to timed automata”, Journal of Systems and Software, Vol. 79, pp. 1456–1468, 2006.
[36] J. Toussaint, F. Simonot-Lion, J. Thomesse, “Time constraints verification methods based on time Petri nets”, Proceedings of the 6th IEEE Computer Society Workshop on Future Trends of Distributed Computing Systems, pp. 262–269, 1997.
[37] D. Lime, O. Roux, C. Seidner, L. Traonouez, “Romeo: a parametric model-checker for Petri nets with stopwatches”, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 54–57, 2009.
[38] Z. Gu, K.G. Shin, “Analysis of event-driven real-time systems with time Petri nets: a translation-based approach”, Proceedings of the IFIP 17th World Computer Congress - TC10 Stream on Distributed and Parallel Embedded Systems: Design and Analysis of Distributed Embedded Systems, pp. 31–40, 2002.
[39] F. Cassez, K. Larsen, “The impressive power of stopwatches”, Proceedings of the 11th International Conference on Concurrency Theory, pp. 138–152, 2000.
[40] O. Roux, A. D´eplanche, “A T-time Petri net extension for real-time task scheduling modelling”, European Journal of Automation, Vol. 36, pp. 973–987, 2002.
[41] O. Roux, D. Lime, “Time Petri nets with inhibitor hyperarcs: formal semantics and state space computation”, Proceedings of the 25th International Conference on Applications and Theory of Petri Nets, Vol. 3099, pp. 371–390, 2004.
[42] Y. Okawa, T. Yoneda, “Schedulability verification of real-time systems with extended time Petri nets”, International Journal of Mini and Microcomputers, Vol. 18, pp. 148–156, 1996.