Abstract
Real-time programs are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. We report on the implementation of our algorithm and we show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.
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
Notes
- 1.
As x and z are clocks their rate is always 1 and omitted in the Table.
- 2.
If x was not reset by i, we would have a constraint \(x_0 = x_{-1}\), with \(x_{-1}\) unconstrained.
- 3.
Uppaal terminates with the result “the language may not be empty”.
- 4.
This can be done using an SMT-solver e.g., Z3.
- 5.
This is the pair returned by Z3 for \(P_0 \wedge P_1 \wedge P_2\).
- 6.
\(\mathcal{I}\) can be infinite but we require the control-flow graph \(\varDelta \) (transition relation) of \(A_P\) to be finite.
- 7.
While difference constraints are strictly disallowed in most definitions of Timed Automata, the method we propose retain its properties regardless of their presence.
- 8.
Existential quantification for the theory of Linear Real Arithmetic is within the theory via Fourier-Motzkin-elimination – hence the solver only needs support for Linear Real Arithmetic for Parameter Synthesis for Stopwatch and Timed Automata.
- 9.
Proving that a system is non-robust requires proving feasibility of infinite traces for ever decreasing \(\epsilon \). We have developed some techniques to do so but this is outside of the scope of this paper.
- 10.
We compare with the EFSynth-algorithm in the Imitator tool as this yielded the lowest computation time in the two terminating instances.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32759-9_6
André, É., Lipari, G., Nguyen, H.G., Sun, Y.: Reachability preservation based parameter synthesis for timed automata. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 50–65. Springer, Cham (2015). doi:10.1007/978-3-319-17524-9_5
Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST 2006, pp. 125–126 (2006)
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time Petri nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211–225. Springer, Heidelberg (2005). doi:10.1007/11603009_17
Beyer, D.: Competition on software verification. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_38
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: The expressive power of time Petri nets. Theor. Comput. Sci. 474, 1–20 (2013)
Byg, J., Jacobsen, M., Jacobsen, L., Jørgensen, K.Y., Møller, M.H., Srba, J.: TCTL-preserving translations from timed-arc Petri nets to networks of timed automata. TCS (2013). doi:10.1016/j.tcs.2013.07.011
Cassez, F., Larsen, K.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 138–152. Springer, Heidelberg (2000). doi:10.1007/3-540-44618-4_12
Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. J. Softw. Syst. 79(10), 1456–1468 (2006)
Cassez, F., Sloane, A.M., Roberts, M., Pigram, M., Suvanpong, P., de Aledo, P.G.: Skink: static analysis of programs in LLVM intermediate representation - (Competition Contribution). In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 380–384. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54580-5_27
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). doi:10.1007/10722167_15
Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24
Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114–129. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75454-1_10
Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31954-2_17
Frehse, G., Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30
Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69–85. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03237-0_7
Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_2
Henzinger, T.A., Ho, P.-H., Wong-toi, H.: HyTech: a model checker for hybrid systems. Softw. Tools Technol. Transf. 1, 460–463 (1997)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)
Kordy, P., Langerak, R., Mauw, S., Polderman, J.W.: A symbolic algorithm for the analysis of robust timed automata. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 351–366. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_25
Sankur, O.: Symbolic quantitative robustness analysis of timed automata. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 484–498. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_48
Wang, W., Jiao, L.: Trace abstraction refinement for timed automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 396–410. Springer, Cham (2014). doi:10.1007/978-3-319-11936-6_28
Acknowledgments
The research leading to these results was made possible by an external stay partially funded by Otto Mønsted Fonden.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Cassez, F., Jensen, P.G., Guldstrand Larsen, K. (2017). Refinement of Trace Abstraction for Real-Time Programs. In: Hague, M., Potapov, I. (eds) Reachability Problems. RP 2017. Lecture Notes in Computer Science(), vol 10506. Springer, Cham. https://doi.org/10.1007/978-3-319-67089-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-67089-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-67088-1
Online ISBN: 978-3-319-67089-8
eBook Packages: Computer ScienceComputer Science (R0)