×

zbMATH — the first resource for mathematics

TCTL-preserving translations from timed-arc Petri nets to networks of timed automata. (English) Zbl 1359.68216
Summary: We present a framework for TCTL-preserving translations between time-dependent modeling formalisms. The framework guarantees that once the original and the translated system are in one-by-many correspondence relation (a notion of behavioral equivalence between timed transition systems) then TCTL properties of the original system can be transformed too while preserving the verification answers. We demonstrate the usability of the technique on two reductions from bounded timed-arc Petri nets to networks for timed automata, providing unified proofs of the translations implemented in the verification tool TAPAAL. We evaluate the efficiency of the approach on a number of experiments: alternating bit protocol, Fischer’s protocol, Lynch-Shavit protocol, MPEG-2 encoder, engine workshop and medical workflow. The results are encouraging and confirm the practical applicability of the approach.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] ISO/IEC 13818-1:2000(E), Information technology—generic coding of moving pictures and associated audio information: Systems, 2000.
[2] Abdulla, P. A.; Deneux, J.; Mahata, P.; Nylén, A., Forward reachability analysis of timed Petri nets, (Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS’04, and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT’04, LNCS, vol. 3253, (2004), Springer-Verlag), 343-362 · Zbl 1109.68509
[3] Abdulla, P. A.; Deneux, J.; Mahata, P.; Nylén, A., Using forward reachability analysis for verification of timed Petri nets, Nordic Journal of Computing, 14, 1-42, (2007) · Zbl 1168.68434
[4] Abdulla, P. A.; Nylén, A., Timed Petri nets and bqos, (Proceedings of the 22nd International Conference on Application and Theory of Petri Nets, ICATPN’01, LNCS, vol. 2075, (2001), Springer-Verlag), 53-70 · Zbl 0986.68092
[5] Alur, R.; Dill, D., Automata for modelling real-time systems, (Proceedings of the 17th International Colloquium on Algorithms, Languages and Programming, ICALP’90, LNCS, vol. 443, (1990), Springer-Verlag), 322-335 · Zbl 0765.68150
[6] Alur, R.; Dill, D., A theory of timed automata, Theoretical Computer Science, 126, 2, 183-235, (1994) · Zbl 0803.68071
[7] Bartlett, K. A.; Scantlebury, R. A.; Wilkinson, P. T., A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, 12, 260-261, (May 1969)
[8] Behrmann, G.; David, A.; Larsen, K. G., A tutorial on \scuppaal, (Bernardo, Marco; Corradini, Flavio, Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT’04, LNCS, vol. 3185, (2004), Springer-Verlag), 200-236 · Zbl 1105.68350
[9] Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; Roux, O. H., Comparison of the expressiveness of timed automata and time Petri nets, (Proc. of FORMATS’05, LNCS, vol. 3829, (2005), Springer), 211-225 · Zbl 1175.68270
[10] Berthomieu, B.; Peres, F.; Vernadat, F., Bridging the gap between timed automata and bounded time Petri nets, (Proc. of FORMATS’06, LNCS, vol. 4202, (2006), Springer), 82-97 · Zbl 1141.68426
[11] Berthomieu, B.; Ribet, P.-O.; Vernadat, F., The tool TINA — construction of abstract state spaces for Petri nets and time Petri nets, International Journal of Production Research, 42, 14, 2741-2756, (2004) · Zbl 1060.68695
[12] Bolognesi, T.; Lucidi, F.; Trigila, S., From timed Petri nets to timed LOTOS, (Proceedings of the IFIP WG 6.1 Tenth International Symposium on Protocol Specification, Testing and Verification, Ottawa, 1990, (1990), North-Holland Amsterdam), 1-14
[13] Boucheneb, H.; Gardey, G.; Roux, O. H., TCTL model checking of time Petri nets, Journal of Logic and Computation, 19, 6, 1509-1540, (2009) · Zbl 1188.68182
[14] Bouyer, P.; Haddad, S.; Reynier, P. A., Timed Petri nets and timed automata: on the discriminating power of Zeno sequences, Information and Computation, 206, 1, 73-107, (2008) · Zbl 1133.68053
[15] Bowden, F. D.J., Modelling time in Petri nets, (Proceedings of the Second Australia-Japan Workshop on Stochastic Models, (1996))
[16] Bozga, M.; Daws, C.; Maler, O.; Olivero, A.; Tripakis, S.; Yovine, S., Kronos: A model-checking tool for real-time systems, (Proceedings of the 10th International Conference on Computer-Aided Verification, CAV’98, LNCS, vol. 1427, (1998), Springer-Verlag), 546-550
[17] Bozga, M.; Graf, S.; Ober, I.; Ober, I.; Sifakis, J., The IF toolset, (Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT’04, LNCS, vol. 3185, (2004), Springer-Verlag), 237-267 · Zbl 1105.68352
[18] Byg, J.; Jørgensen, K. Y.; Srba, J., An efficient translation of timed-arc Petri nets to networks of timed automata, (Proc. of ICFEM’09, LNCS, vol. 5885, (2009), Springer), 698-716
[19] Byg, J.; Jørgensen, K. Y.; Srba, J., TAPAAL: editor, simulator and verifier of timed-arc Petri nets, (Proc. of ATVA’09, LNCS, vol. 5799, (2009), Springer), 84-89
[20] Cambronero, M. E.; Ravn, A. P.; Valero, V., Using UPPAAL to analyze an MPEG-2 algorithm, (Proc. of VII Workshop Brasileiro de Tempo Real, (2005)), 73-82
[21] Cassez, F.; Roux, O. H., Structural translation from time Petri nets to timed automata, The Journal of Systems and Software, 79, 10, 1456-1468, (2006)
[22] Christov, S. C.; Avrunin, G. S.; Clarke, L. A.; Osterweil, L. J.; Henneman, E. A., A benchmark for evaluating the applicability of software engineering techniques to the improvement of medical processes, (Proceedings of the 2010 ICSE Workshop on Software Engineering in Health Care, SEHC’10, (2010), ACM Press), 50-56
[23] David, A.; Jacobsen, L.; Jacobsen, M.; Jørgensen, K. Y.; Møller, M. H.; Srba, J., TAPAAL 2.0: integrated development environment for timed-arc Petri nets, (Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’12, LNCS, vol. 7214, (2012), Springer-Verlag), 492-497 · Zbl 1352.68181
[24] Dong, J. S.; Hao, P.; Qin, S.; Sun, J.; Yi, W., Timed automata patterns, IEEE Transactions on Software Engineering, 34, 6, 844-859, (2008)
[25] Gardey, G.; Lime, D.; Magnin, M.; Roux, O. H., Romeo: A tool for analyzing time Petri nets, (Proc. of CAV’05, LNCS, vol. 3576, (2005), Springer), 418-423 · Zbl 1081.68618
[26] Hanisch, H. M., Analysis of place/transition nets with timed-arcs and its application to batch process control, (Proceedings of the 14th International Conference on Application and Theory of Petri Nets, ICATPN’93, LNCS, vol. 691, (1993)), 282-299
[27] Heitmann, F.; Moldt, D.; Mortensen, K. H.; Rölke, H., Petri nets tools database quick overview (from Petri net world), Accessed: 29.4.2013
[28] Jacobsen, L.; Jacobsen, M.; Møller, M. H.; Srba, J., A framework for relating timed transition systems and preserving TCTL model checking, (Proceedings of the 7th European Performance Engineering Workshop, EPEW’10, LNCS, vol. 6342, (2010), Springer-Verlag), 83-98
[29] Jacobsen, L.; Jacobsen, M.; Møller, M. H.; Srba, J., Verification of timed-arc Petri nets, (Proceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM’11, LNCS, vol. 6543, (2011), Springer-Verlag), 46-72 · Zbl 1298.68175
[30] Janowska, A.; Janowski, P.; Wróblewski, D., Translation of intermediate language to timed automata with discrete data, Fundamenta Informaticae, 85, 1-4, 235-248, (2008) · Zbl 1158.68020
[31] Lamport, L., A fast mutual exclusion algorithm, ACM Transactions on Computer Systems, 5, 1, 1-11, (1987)
[32] Laroussinie, F.; Larsen, K. G., CMC: A tool for compositional model-checking of real-time systems, (Proceedings of the FIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, FORTE XI, and Protocol Specification, Testing and Verification, PSTV XVIII, (1998), Kluwer, B.V.), 439-456
[33] Lynch, N.; Shavit, N., Timing-based mutual exclusion, (Proceedings of the 13th IEEE Real-Time Systems Symposium, (1992)), 2-11
[34] Lynch, W. C., Computer systems: reliable full-duplex file transmission over half-duplex telephone line, Communications of the ACM, 11, 407-410, (June 1968)
[35] Merlin, P. M., A study of the recoverability of computing systems, (1974), University of California Irvine, CA, USA, PhD thesis
[36] Merlin, P. M.; Faber, D. J., Recoverability of communication protocols: implications of a theoretical study, IEEE Transactions on Communications, 24, 9, 1036-1043, (1976) · Zbl 0362.68096
[37] Namjoshi, K. S., A simple characterization of stuttering bisimulation, (Ramesh, S.; Sivakumar, G., Foundations of Software Technology and Theoretical Computer Science, LNCS, vol. 1346, (1997), Springer-Verlag), 284-296
[38] Pelayo, F. L.; Cuartero, F.; Valero, V.; Macia, H.; Pelayo, M. L., Applying timed-arc Petri nets to improve the performance of the MPEG-2 encoding algorithm, (Proceedings of the 10th International Multimedia Modelling Conference, MMM’04, (2004), IEEE Computer Society), 49-56
[39] Pelayo, F. L.; Cuartero, F.; Valero, V.; Pelayo, M. L.; Merayo, M. G., How does the memory work? by timed-arc Petri nets, (Proceedings of the 4th IEEE International Conference on Cognitive Informatics, ICCI’05, (2005)), 128-135
[40] Penczek, W.; Pólrola, A., Advances in verification of time Petri nets and timed automata: A temporal logic approach, (2006), Springer-Verlag · Zbl 1110.68087
[41] Penczek, W.; Pólrola, A., Advances in verification of time Petri nets and timed automata: A temporal logic approach, Studies in Computational Intelligence, vol. 20, (2006), Springer · Zbl 1110.68087
[42] Petri, C. A., Kommunikation mit automaten, (1962), TU Darmstadt, PhD thesis
[43] Ramchandani, C., Performance evaluation of asynchronous concurrent systems by timed Petri nets, (1973), Massachusetts Institute of Technology Cambridge, PhD thesis
[44] Sifakis, J., Use of Petri nets for performance evaluation, (Proceedings of the Third International Symposium IFIP W.G. 7.3., Measuring, Modelling and Evaluating Computer Systems, Bonn-Bad Godesberg, 1977, (1977), Elsevier Science Publishers Amsterdam), 75-93
[45] Sifakis, J.; Yovine, S., Compositional specification of timed systems, (Proc. of STACS’96, LNCS, vol. 1046, (1996), Springer), 347-359 · Zbl 1379.68240
[46] Srba, J., Timed-arc Petri nets vs. networks of timed automata, (Proceedings of the 26th International Conference on Application and Theory of Petri Nets, ICATPN 2005, LNCS, vol. 3536, (2005), Springer-Verlag), 385-402 · Zbl 1128.68069
[47] Srba, J., Comparing the expressiveness of timed automata and timed extensions of Petri nets, (Proc. of FORMATS’08, LNCS, vol. 5215, (2008), Springer), 15-32 · Zbl 1171.68579
[48] Valero, V.; Cuartero, F.; de Frutos Escrig, D., On non-decidability of reachability for timed-arc Petri nets, (Proceedings of the 8th International Workshop on Petri Net and Performance Models, PNPM’99, (1999)), 188-196
[49] Valero, V.; Pardo, J. J.; Cuartero, F., Translating TPAL specifications into timed-arc Petri nets, (Proceedings of the 23rd International Conference on Applications and Theory of Petri Nets, ICATPN’02, LNCS, vol. 2360, (2002), Springer-Verlag), 414-433 · Zbl 1047.68090
[50] Valero, V.; Pelayo, F. L.; Cuartero, F.; Cazorla, D., Specification and analysis of the MPEG-2 video encoder with timed-arc Petri nets, Electronic Notes Theoretical Computer Science, 66, 2, (2002)
[51] Wang, J., Timed Petri nets, theory and application, (1998), Kluwer Academic Publishers · Zbl 0924.68147
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.