SCIENCE CHINA Information Sciences, Volume 61, Issue 5: 052106(2018) https://doi.org/10.1007/s11432-017-9152-x

## Symbolic model checking for discrete real-time systems

• AcceptedJun 29, 2017
• PublishedDec 26, 2017
Share
Rating

### Abstract

A considerably large class of critical applications run in distributed and real-time environments, and most of the correctness requirements of such applications must be expressed by time-critical properties. To enable the specification and verification of these properties in both qualitative and quantitative manners, we propose a new real-time temporal logic $\rm~{RTCTL^*}$, by incorporating both the quantitative (bounded) future and past temporal operators from the qualitative temporal logic $\rm~{CTL^*}$. First, we propose a symbolic method for constructing the temporal tester for arbitrary principally temporal formulas. A temporal tester is constructed as a non-deterministic transducer with a fresh boolean output variable, such that at any position the output variable is set to be true if and only if the corresponding formula holds starting from that position. Then we propose a symbolic model checking method for $\rm~{RTCTL^*}$ over finite-state transition systems with weak fairness constraints based on the compositionality of testers. The soundness and completeness of the model checking method, the expressiveness of $\rm~{RTCTL^*}$, and the complexity of the tester construction are described and proven. We have already implemented an efficient model checking prototype for the real-time linear temporal logic $\rm~{RTLTL}$, which is a quantifier-free version of $\rm~{RTCTL^*}$, by building upon the NuSMV model checker. The theoretical and the experimental results from the prototype both confirm that for checking bounded temporal formulae of the form $f\texttt{U}_{[0,b]}g$ or $f\texttt{S}_{[0,b]}g$, our method performs exponentially better than the translation-based method in NuSMV.

### References

[1] Clarke E M, Grumberg O, Peled D A. Model Checking London: The MIT Press, 2000. Google Scholar

[2] Goranko V, Galton A. Temporal logic. In: The Stanford Encyclopedia of Philosophy San Francisco: Metaphysics Research Lab, Stanford University, 2015. Google Scholar

[3] Holzmann G J. The SPIN Model Checker-Primer and Reference Manual Boston: Addison-Wesley, 2004. Google Scholar

[4] Cimatti A, Clarke E M, Giunchiglia E, et al. Nusmv 2: an opensource tool for symbolic model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002) Berlin: Springer, 2002. 359--364. Google Scholar

[5] McMillan K L. Symbolic Model Checking Norwell: Kluwer Academic Publisher, 1993. Google Scholar

[6] Pnueli A, Sa'ar Y, Zuck L D. Jtlv: a framework for developing verification algorithms. In: Proceedings of the 22th International Conference on Computer Aided Verification (CAV 2010) Berlin: Springer, 2010. 171--174. Google Scholar

[7] Su K, Sattar A, Luo X. Model Checking Temporal Logics of Knowledge Via OBDDs1. Comput J, 2007, 50: 403-420 CrossRef Google Scholar

[8] Larsen K G, Pettersson P, Yi W. Uppaal in a nutshell. STTT, 1997, 1: 134-152 CrossRef Google Scholar

[9] Henzinger T A, Ho P H, Wong-Toi H. HYTECH: a model checker for hybrid systems. STTT, 1997, 1: 110-122 CrossRef Google Scholar

[10] Bozga M, Daws C, Maler O, et al. Kronos: a model-checking tool for real-time systems. In: Proceedings of the 10th International Conference on Computer Aided Verification (CAV 1998). London: Springer-Verlag, 1998. 546--550. Google Scholar

[11] Morbé G, Scholl C. Fully symbolic TCTL model checking for complete and incomplete real-time systems. Sci Comput Programming, 2015, 111: 248-276 CrossRef Google Scholar

[12] Alur R, Courcoubetis C, Dill D. Model-Checking in Dense Real-Time. Inf Computation, 1993, 104: 2-34 CrossRef Google Scholar

[13] Alur R, Henzinger T A. Real-Time Logics: Complexity and Expressiveness. Inf Computation, 1993, 104: 35-77 CrossRef Google Scholar

[14] Alur R, Henzinger T A. A really temporal logic. J ACM, 1994, 41: 181-203 CrossRef Google Scholar

[15] Alur R, Feder T, Henzinger T A. The benefits of relaxing punctuality. J ACM, 1996, 43: 116-146 CrossRef Google Scholar

[16] Aceto L, Laroussinie F. Is your model checker on time? On the complexity of model checking for timed modal logics. J Log Algebr Program, 2002, 52: 7--51. Google Scholar

[17] Bouyer P, Fahrenberg U, Larsen K G, et al. Model checking real-time systems. In: Handbook of Model Checking Berlin: Springer-Verlag, 2017. Google Scholar

[18] Lomuscio A, Qu H, Raimondi F. MCMAS: an open-source model checker for the verification of multi-agent systems. Int J Softw Tools Technol Transfer, 2017, 19: 9-30 CrossRef Google Scholar

[19] Bryant R E. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv, 1992, 24: 293-318 CrossRef Google Scholar

[20] Emerson E A, Mok A K, Sistla A P. Quantitative temporal reasoning. Real-Time Syst, 1992, 4: 331-352 CrossRef Google Scholar

[21] Fruth M. Formal verification of embedded real-time systems Dissertation for Ph.D. Degree. Dresden: TU Dresden, 2005. Google Scholar

[22] Pnueli A, Zaks A. On the merits of temporal testers. In: 25 Years of Model Checking: History, Achievements, Perspectives Berlin: Springer, 2008. 172--195. Google Scholar

[23] Finkbeiner B, Rabe M N, Sánchez C. Algorithms for model checking HyperLTL and HyperCTL$^*$. In: Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015) Berlin: Springer, 2015. 30--48. Google Scholar

[24] Cimatti A, Griggio A, Mover S, et al. Verifying LTL properties of hybrid systems with k-liveness. In: Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2014) Berlin: Springer, 2014. 424--440. Google Scholar

[25] Cook B, Khlaaf H, Piterman N. On automation of CTL$^*$ verification for infinite-state systems. In: Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015) Berlin: Springer, 2015. 13--29. Google Scholar

[26] Zhang N, Duan Z, Tian C. Model checking concurrent systems with MSVL. Sci China Inf Sci, 2016, 59: 118101 CrossRef Google Scholar

[27] Immler F. Verified reachability analysis of continuous systems. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). Berlin: Springer, 2015. 37--51. Google Scholar

[28] Lin W, Wu M, Yang Z F, et al. Exact safety verification of hybrid systems using sums-of-squares representation. Sci China Inf Sci 2014, 57: 052101. Google Scholar

• Figure 1

The (bounded) future and past temporal operators derived from $\rm~RTCTL^*$.

• Figure 2

The tester $T_{f\texttt{U}_{[0,b]}g}$.

• Figure 3

The tester $T_{f~\texttt{S}_{[0,b]}g}$.

• Figure 4

Composition of transducers to form the tester for subformula $\beta=(\top~\texttt{U}_{[0,k]}{\rm~ack})~\land~\neg(\top\texttt{U}({\rm~ack}\land~\texttt{X}\neg(\top~\texttt{U}_{[0,k-1]}{\rm~ack})~))$.

• Figure 5

(Color online) Model checking framework for $\rm~{RTLTL}$.

• Figure 6

The NuSMV modules representing the testers for the basic temporal operators $\texttt{X}$, $\texttt{Y}$, $\texttt{U}$, $\texttt{S}$, $\texttt{U}_{[0,b]}$, and $\texttt{S}_{[0,b]}$.

• Figure 7

The NuSMV input programs for testing.

• Figure 8

(Color online) Experimental comparison for checking $\texttt{G}_{[0,mb]}p~$ in program (1) using NuSMV and our method. (a) Total verification time; (b) memory in use; (c) number of BDD variables; (d) peak number of nodes.

• Figure 9

(Color online) Experimental comparison for checking $\texttt{G}(c=cb~\rightarrow~\texttt{O}_{[0,mb]}p)$ in program (2) using NuSMV and our method. (a) Total verification time; (b) memory in use; (c) number of BDD variables; (d) peak number of nodes.

Citations

• #### 0

Altmetric

Copyright 2019 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有