×

Model checking duration calculus: a practical approach. (English) Zbl 1151.68487


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aceto L, Bouyer P, Burgueño A, Larsen KG (2003) The power of reachability testing for timed automata. Theor Comput Sci 300(1–3): 411–475 · Zbl 1023.68060
[2] Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2): 183–235 · Zbl 0803.68071
[3] Bouajjani A, Lakhnech Y, Robbana R (1995) From duration calculus to linear hybrid automata. In: Wolper P (eds) CAV, LNCS, vol 939. Springer, Heidelberg, pp 196–210
[4] Ball T, Majumdar R, Millstein T, Rajamani S (2001) Automatic predicate abstraction of C programs. In: PLDI, volume 36 of ACM SIGPLAN Notices. ACM Press, New York, pp 203–213
[5] Brückner I (2007) Slicing Concurrent Real-Time System Specifications for Verification. In: Davies J, Gibbons J(eds) Integrated Formal Methods, LNCS, vol 4591. Springer, Heidelberg, pp 54–74 · Zbl 1213.68366
[6] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Emerson EA, Sistla AP(eds) CAV, LNCS, vol 1855. Springer, Heidelberg, pp 154–169 · Zbl 0974.68517
[7] Cook B, Podelski A, Rybalchenko A (2005) Abstraction refinement for termination. In: SAS, LNCS, vol 3672. Springer, Heidelberg, pp 87–101 · Zbl 1141.68365
[8] Dierks H, Lettrari M (2002) Constructing test automata from graphical real-time requirements. In: Damm W, Olderog E-R(eds) FTRTFT, LNCS, vol 2469. Springer, Heidelberg, pp 433–453 · Zbl 1278.68167
[9] ECSAG. ERTMS/ETCS Functional requirements specification (1999)
[10] ERTMS User Group, UNISIG. ERTMS/ETCS System requirements specification (2002)
[11] Fränzle M, Hansen MR (2007) Deciding an interval logic with accumulated durations. In: TACAS, LNCS, vol 4424. Springer, Heidelberg, pp 201–215 · Zbl 1186.03055
[12] Faber J, Jacobs S, Sofronie-Stokkermans V (2007) Verifying CSP-OZ-DC specifications with complex data types and timing parameters. In: Davies J, Gibbons J(eds) Integrated Formal Methods. LNCS, vol 4591. Springer, Heidelberg, pp 233–252 · Zbl 1213.68374
[13] Fränzle M (2004) Model-checking dense-time duration calculus. Formal Asp Comput 16(2): 121–139 · Zbl 1084.68071
[14] Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: Grumberg O (ed.) CAV, vol 1254. Springer, Heidelberg, pages 72–83
[15] Hansen M (2006) DC with nominals. Personal communication, March (2006)
[16] Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: Jones ND, Leroy X(eds) POPL. ACM Press, New York, pp 232–244 · Zbl 1325.68147
[17] Hermanns H, Jansen DN, Usenko YS (2005) From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. In: WOSP. ACM Press, New York, pp 13–23
[18] Hoenicke J, Maier P (2005) Model-checking of specifications integrating processes, data and time. In: Fitzgerald JS, Hayes IJ, Tarlecki A(eds) FM, LNCS, vol 3582. Springer, Heidelberg, pp 465–480 · Zbl 1120.68417
[19] Hoenicke J, Meyer R, Faber J (2006) PEA toolkit home page. http://csd.informatik.uni-oldenburg.de/projects/epea.html
[20] Hoenicke J, Olderog ER (2002) CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic J Comput 9 · Zbl 1088.68643
[21] Hoare CAR (1985) Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs · Zbl 0637.68007
[22] Hoenicke J (2006) Combination of Processes, Data, and Time. Ph.D. thesis, University of Oldenburg
[23] Krishna SN, Pandya PK (2005) Modal strength reduction in quantified discrete duration calculus. In: Ramanujam R, Sen S(eds) FSTTCS, LNCS, vol 3821. Springer, Heidelberg, pp 444–456 · Zbl 1172.03320
[24] McMillan KL Jr (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr, Somenzi F(eds) CAV, LNCS, vol 2725. Springer, Heidelberg, pp 1–13 · Zbl 1278.68184
[25] Meyer R, Faber J, Rybalchenko A (2006) Model checking duration calculus: A practical approach. In: Barkaoui K, Cavalcanti A, Cerone A(eds) ICTAC, LNCS, vol 4281. Springer, Heidelberg, pp 332–346 · Zbl 1168.68425
[26] Pandya PK (2002) Interval duration logic: Expressiveness and decidability. ENTCS 65(6) · Zbl 1270.68175
[27] Platzer A (2007) Differential dynamic logic for verifying parametric hybrid systems. In: Olivetti N.(eds) TABLEAUX, LNCS, vol 4548. Springer, Heidelberg, pp 216–232 · Zbl 1132.68478
[28] Podelski A, Rybalchenko A (2005) Transition predicate abstraction and fair termination. In: POPL. ACM Press, New York, pp 132–144 · Zbl 1369.68152
[29] Podelski A, Rybalchenko A (2007) ARMC: the logical choice for software model checking with abstraction refinement. In: PADL, LNCS, vol 4281. Springer, Heidelberg, pp 245–259
[30] Ravn AP (1994) Design of Embedded Real-Time Computing Systems. Ph.D. thesis, Technical University of Denmark
[31] Roscoe AW (1998) Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs
[32] Rybalchenko A, Sofronie-Stokkermans V (2007) Constraint solving for interpolation. In: VMCAI, LNCS, vol 4349. Springer, Heidelberg, pp. 346–362 · Zbl 1132.68480
[33] Rybalchenko A (2007) ARMC. http://www.mpi-sws.mpg.de/\(\sim\)rybal/armc
[34] Smith G (2000) The Object-Z Specification Language. Kluwer, Dordrecht · Zbl 0944.68124
[35] Uppaal home page. University of Aalborg and University of Uppsala. http://www.uppaal.com , 1995–2005
[36] Vardi MY (1991) Verification of concurrent programs: The automata-theoretic framework. Ann Pure Appl Logic 51(1–2): 79–98 · Zbl 0725.03013
[37] Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: LICS. IEEE Computer Society, pp 332–344
[38] Zhou C, Hansen MR (2004) Duration Calculus. Springer, Heidelberg · Zbl 1071.68062
[39] Zimmermann A, Hommel G (2005) Towards modeling and evaluation of ETCS real-time communication and operation. J Syst Softw 77(1): 47–54 · Zbl 05434140
[40] Zhou C, Hansen MR, Sestoft P (1993) Decidability and undecidability results for duration calculus. In: Enjalbert P, Finkel A, Wagner KW(eds) STACS, LNCS, vol 665. Springer, Heidelberg, pp 58–68 · Zbl 0811.68115
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.