Abstract
State-space explosion is a major obstacle in verification of time-critical distributed systems. An important factor with a negative influence on the tractability of the analysis is the size of constants that clocks are compared to. This problem is particularly accented in explicit state-space exploration techniques. We suggest an approximation method for reducing the size of constants present in the model. The proposed method is developed for Timed-Arc Petri Nets and creates an under-approximation or an over-approximation of the model behaviour. The verification of approximated Petri net models can be considerably faster but it does not in general guarantee conclusive answers. We implement the algorithms within the open-source model checker TAPAAL and demonstrate on a number of experiments that our approximation techniques often result in a significant speed-up of the verification.
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
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Itai, A., Kurshan, R., Yannakakis, M.: Timing verification by successive approximation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 137–150. Springer, Heidelberg (1993)
Andersen, M., Gatten Larsen, H., Srba, J., Grund Sørensen, M., Haahr Taankvist, J.: Verification of liveness properties on closed timed-arc Petri nets. In: Kučera, A., Henzinger, T.A., Nešetřil, J., Vojnar, T., Antoš, D. (eds.) MEMICS 2012. LNCS, vol. 7721, pp. 69–81. Springer, Heidelberg (2013)
Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 470–484. Springer, Heidelberg (1998)
Bolognesi, T., Lucidi, F., Trigila, S.: From timed Petri nets to timed LOTOS. In: IFIP WG 6.1 Tenth International Symposium on Protocol Specification, Testing and Verification, pp. 1–14. North-Holland, Amsterdam (1990)
Bozga, M., Maler, O., Tripakis, S.: Efficient verification of timed automata using dense and discrete time semantics. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 125–141. Springer, Heidelberg (1999)
Cicirelli, F., Furfaro, A., Nigro, L.: Model checking time-dependent system specifications using time stream Petri nets and UPPAAL. Applied Mathematics and Computation 218(16), 8160–8186 (2012)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
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. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492–497. Springer, Heidelberg (2012)
David, A., Jacobsen, L., Jacobsen, M., Srba, J.: A forward reachability algorithm for bounded timed-arc Petri nets. In: SSV 2012. EPTCS, vol. 102, pp. 125–140. Open Publishing Association (2012)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
Dill, D.L., Wong-Toi, H.: Verification of real-time systems by successive over and under approximation. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 409–422. Springer, Heidelberg (1995)
Drægert, A., Kaysen, A.C., Byrdal Kjær, J., Mikkelsen, F.B., Nduru, C., Petersen, D.S.: LEGO car safety systems. 5th Semester Software Engineer Project Report, Aalborg University (2014)
Hanisch, H.M.: Analysis of place/transition nets with timed-arcs and its application to batch process control. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 282–299. Springer, Heidelberg (1993)
Jensen, P.G., Larsen, K.G., Srba, J., Sørensen, M.G., Taankvist, J.H.: Memory efficient data structures for explicit verification of timed systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 307–312. Springer, Heidelberg (2014)
Jørgensen, K.Y., Larsen, K.G., Srba, J.: Time-darts: A data structure for verification of closed timed automata. In: SSV 2012. EPTCS, vol. 102, pp. 141–155. Open Publishing Association (2012)
Marques Jr., A.P., Ravn, A.P., Srba, J., Vighio, S.: Model-checking web services business activity protocols. International Journal on Software Tools for Technology Transfer (STTT) 15(2), 125–147 (2013)
Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005)
Larsen, K.G., Behrmann, G., Skou, A.: Exercises for UPPAAL (2008), http://www.cs.aau.dk/~bnielsen/TOV08/ESV04/exercises
Lee, W., Pardo, A., Jang, J.-Y., Hachtel, G., Somenzi, F.: Tearing based automatic abstraction for CTL model checking. In: ICCAD 1996, pp. 76–81. IEEE Computer Society (1996)
Merlin, P.M., Faber, D.J.: Recoverability of communication protocols: Implications of a theoretical study. IEEE Trans. on Comm. 24(9), 1036–1043 (1976)
Murata, T.: State equation, controllability, and maximal matchings of Petri nets. IEEE Trans. on Automatic Control 22(3), 412–416 (1977)
Pardo, A., Hachtel, G.D.: Incremental CTL model checking using BDD subsetting. In: DAC 1998, pp. 457–462. ACM (1998)
Popova-Zeugmann, L.: On time Petri nets. Elektronische Informationsverarbeitung und Kybernetik 27(4), 227–244 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Viesmose Birch, S., Stig Jacobsen, T., Jon Jensen, J., Moesgaard, C., Nørgaard Samuelsen, N., Srba, J. (2014). Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets. In: Legay, A., Bozga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2014. Lecture Notes in Computer Science, vol 8711. Springer, Cham. https://doi.org/10.1007/978-3-319-10512-3_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-10512-3_17
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10511-6
Online ISBN: 978-3-319-10512-3
eBook Packages: Computer ScienceComputer Science (R0)