{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:30:07Z","timestamp":1762522207179,"version":"3.37.3"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,9,3]],"date-time":"2018-09-03T00:00:00Z","timestamp":1535932800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Comb Optim"],"published-print":{"date-parts":[[2019,5]]},"DOI":"10.1007\/s10878-018-0343-1","type":"journal-article","created":{"date-parts":[[2018,9,3]],"date-time":"2018-09-03T07:55:56Z","timestamp":1535961356000},"page":"1191-1215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying a scheduling protocol of safety-critical systems"],"prefix":"10.1007","volume":"37","author":[{"given":"Meng","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2772-1433","authenticated-orcid":false,"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongwei","family":"Du","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,3]]},"reference":[{"key":"343_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed W, Hasan O, Tahar S (2015) Formal reliability analysis of wireless sensor network data transport protocols using HOL. In: IEEE international conference on wireless and mobile computing, networking and communications, pp 217\u2013224","DOI":"10.1109\/WiMOB.2015.7347964"},{"issue":"4","key":"343_CR2","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10817-010-9172-3","volume":"45","author":"D Angeletti","year":"2010","unstructured":"Angeletti D, Giunchiglia E, Narizzano M, Puddu A, Sabina S (2010) Using bounded model checking for coverage analysis of safety-critical software in an industrial setting. J Autom Reason 45(4):397\u2013414","journal-title":"J Autom Reason"},{"key":"#cr-split#-343_CR3.1","doi-asserted-by":"crossref","unstructured":"Armando A, Mantovani J, Platania L (2006) Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari A","DOI":"10.1007\/11691617_9"},{"key":"#cr-split#-343_CR3.2","unstructured":"(ed) Model checking software. SPIN 2006. Lecture notes in computer science, vol 3925. Springer, Berlin, Heidelberg, pp 146-162"},{"issue":"6","key":"343_CR4","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1016\/j.ipl.2016.02.001","volume":"116","author":"C Bernardeschi","year":"2016","unstructured":"Bernardeschi C, Domenici A (2016) Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system. Inf Process Lett 116(6):409\u2013415","journal-title":"Inf Process Lett"},{"key":"343_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development","author":"Y Bertot","year":"2004","unstructured":"Bertot Y, Cast\u00e9ran P (2004) Interactive theorem proving and program development. Springer, New York"},{"key":"343_CR6","doi-asserted-by":"crossref","unstructured":"Beyer D, Keremoglu ME (2011) CPAchecker: a tool for configurable software verification. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification. CAV 2011. Lecture notes in computer science, vol 6806. Springer, Berlin, Heidelberg, pp 184\u2013190","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"343_CR7","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-24690-6_6","volume-title":"Software engineering and formal methods","author":"JO Blech","year":"2011","unstructured":"Blech JO, Ould Biha S (2011) Verification of PLC properties based on formal semantics in Coq. In: Barthe G, Pardo A, Schneider G (eds) Software engineering and formal methods. Springer, Berlin, pp 58\u201373"},{"key":"343_CR8","doi-asserted-by":"crossref","unstructured":"Brockschmidt M, Cook B, Ishtiaq S, Khlaaf H, Piterman N (2016) T2: temporal property verification. In: International conference on tools and algorithms for the construction and analysis of systems, Springer, pp 387\u2013393","DOI":"10.1007\/978-3-662-49674-9_22"},{"key":"343_CR9","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1016\/j.engfailanal.2017.06.034","volume":"82","author":"L Chen","year":"2017","unstructured":"Chen L, Jiao J, Wei Q, Zhao T (2017) An improved formal failure analysis approach for safety-critical system based on MBSA. Eng Fail Anal 82:713\u2013725","journal-title":"Eng Fail Anal"},{"issue":"4","key":"343_CR10","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti A, Clarke E, Giunchiglia F, Roveri M (2000) NuSMV: a new symbolic model checker. Int J Softw Tools Technol Transf 2(4):410\u2013425","journal-title":"Int J Softw Tools Technol Transf"},{"key":"343_CR11","doi-asserted-by":"crossref","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: International conference on computer aided verification, Springer, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"issue":"2","key":"343_CR12","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst (TOPLAS) 8(2):244\u2013263","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"key":"343_CR13","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT press, Cambridge"},{"key":"343_CR14","doi-asserted-by":"crossref","unstructured":"Dietsch D, Heizmann M, Langenfeld V, Podelski A (2015) Fairness modulo theory: a new approach to LTL software model checking. In: Computer aided verification","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"343_CR15","unstructured":"Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle upon Tyne"},{"key":"343_CR16","volume-title":"Temporal logic and temporal logic programming","author":"Z Duan","year":"2005","unstructured":"Duan Z (2005) Temporal logic and temporal logic programming. Science Press, Henderson"},{"issue":"3","key":"343_CR17","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/BF02944904","volume":"19","author":"Z Duan","year":"2004","unstructured":"Duan Z, Koutny M (2004) A framed temporal logic programming language. J Comput Sci Technol 19(3):341\u2013351","journal-title":"J Comput Sci Technol"},{"key":"343_CR18","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.tcs.2014.02.011","volume":"554","author":"Z Duan","year":"2014","unstructured":"Duan Z, Tian C (2014) A practical decision procedure for propositional projection temporal logic with infinite models. Theor Comput Sci 554:169\u2013190","journal-title":"Theor Comput Sci"},{"issue":"1","key":"343_CR19","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z Duan","year":"2008","unstructured":"Duan Z, Yang X, Koutny M (2008) Framed temporal logic programming. Sci Comput Program 70(1):31\u201361","journal-title":"Sci Comput Program"},{"key":"343_CR20","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1016\/j.tcs.2012.01.026","volume":"497","author":"Z Duan","year":"2013","unstructured":"Duan Z, Zhang N, Koutny M (2013) A complete proof system for propositional projection temporal logic. Theor Comput Sci 497:84\u2013107 (Combinatorial Algorithms and Applications)","journal-title":"Theor Comput Sci"},{"key":"343_CR21","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.08.039","volume-title":"A canonical form based decision procedure and model checking approach for propositional projection temporal logic","author":"Z Duan","year":"2016","unstructured":"Duan Z, Tian C, Zhang N (2016) A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Elsevier, New York"},{"key":"343_CR22","first-page":"317","volume":"89","author":"MJC Gordon","year":"1993","unstructured":"Gordon MJC, Melham TF (1993) Introduction to HOL: a theorem proving environment for higher order logic. IEEE Trans Reliab 89:317\u2013320","journal-title":"IEEE Trans Reliab"},{"issue":"5","key":"343_CR23","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Software Eng 23(5):279\u2013295","journal-title":"IEEE Trans Software Eng"},{"key":"343_CR24","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-71067-7_4","volume-title":"Theorem proving in higher order logics","author":"M Kaufmann","year":"2008","unstructured":"Kaufmann M, Moore JS (2008) An ACL2 tutorial. In: Mohamed OA, Mu\u00f1oz C, Tahar S (eds) Theorem proving in higher order logics. Springer, Berlin, pp 17\u201321"},{"key":"343_CR25","doi-asserted-by":"crossref","unstructured":"Kroening D, Tautschnig M (2014) CBMC\u2013C bounded model checker. In: Tools and algorithms for construction and analysis of systems","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"343_CR26","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569845","volume-title":"Higher order logic and hardware verification","author":"T Melham","year":"1993","unstructured":"Melham T (1993) Higher order logic and hardware verification. Cambridge University Press, Cambridge"},{"key":"343_CR27","doi-asserted-by":"crossref","unstructured":"Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: International conference on automated deduction, Springer, pp 748\u2013752","DOI":"10.1007\/3-540-55602-8_217"},{"key":"343_CR28","volume-title":"Isabelle\u2013a generic theorem prover. Of LNCS","author":"LC Paulson","year":"1994","unstructured":"Paulson LC (1994) Isabelle\u2013a generic theorem prover. Of LNCS. Springer, New York"},{"key":"343_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, 1977, IEEE, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"343_CR30","first-page":"301","volume-title":"Modeling and security analysis of a commercial real-time operating system kernel","author":"RJ Richards","year":"2010","unstructured":"Richards RJ (2010) Modeling and security analysis of a commercial real-time operating system kernel. Springer, Boston, pp 301\u2013322"},{"key":"343_CR31","unstructured":"Spichkova M, Blech JO, Herrmann P, Schmidt H (2014) Modeling spatial aspects of safety-critical systems with focus-st. In: The workshop on model driven engineering, pp 49\u201358"},{"key":"343_CR32","doi-asserted-by":"crossref","unstructured":"Sun J, Liu Y, Dong JS (2008) Model checking CSP revisited: introducing a process analysis toolkit. In: international symposium on leveraging applications of formal methods, verification and validation, Springer, pp 307\u2013322","DOI":"10.1007\/978-3-540-88479-8_22"},{"key":"343_CR33","doi-asserted-by":"crossref","unstructured":"Tuan LA, Man CZ, Quan TT (2010) Modeling and verification of safety critical systems: a case study on pacemaker. In: Fourth international conference on secure software integration and reliability improvement, pp 23\u201332","DOI":"10.1109\/SSIRI.2010.28"},{"issue":"1\u20132","key":"343_CR34","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"MY Vardi","year":"1991","unstructured":"Vardi MY (1991) Verification of concurrent programs: the automata-theoretic framework. Ann Pure Appl Logic 51(1\u20132):79\u201398","journal-title":"Ann Pure Appl Logic"},{"key":"343_CR35","doi-asserted-by":"crossref","unstructured":"Wang M, Tian C, Duan Z (2017) Full regular temporal property verification as dynamic program execution. In: Proceedings of the 39th international conference on software engineering, ICSE 2017, Buenos Aires, Argentina, May 20\u201328, 2017\u2014companion volume, pp 226\u2013228","DOI":"10.1109\/ICSE-C.2017.98"},{"issue":"5","key":"343_CR36","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/s11704-016-6059-4","volume":"11","author":"X Wang","year":"2017","unstructured":"Wang X, Tian C, Duan Z, Zhao L (2017) MSVL: a typed language for temporal logic programming. Front Comput Sci 11(5):762\u2013785","journal-title":"Front Comput Sci"},{"key":"343_CR37","doi-asserted-by":"publisher","unstructured":"Yang K, Duan Z, Tian C, Zhang N (2017) A compiler for MSVL and its applications. Theor Comput Sci. \n                    https:\/\/doi.org\/10.1016\/j.tcs.2017.07.032","DOI":"10.1016\/j.tcs.2017.07.032"},{"key":"343_CR38","first-page":"356","volume":"3668","author":"X Yang","year":"2007","unstructured":"Yang X, Duan Z (2007) Operational semantics of framed temporal logic programs. Logic Program Proceed 3668:356\u2013370","journal-title":"Logic Program Proceed"},{"key":"343_CR39","unstructured":"Yasmeen A, Feigh KM, Gelman G, Gunter EL (2012) Formal analysis of safety-critical system simulations. In: International conference on application and theory of automation in command and control systems, ATACCS \u201912, London, UK, May 29\u201331, 2012, pp 71\u201381"},{"issue":"2","key":"343_CR40","first-page":"1","volume":"31","author":"N Zhang","year":"2014","unstructured":"Zhang N, Yang M, Gu B, Duan Z, Tian C (2014) Verifying safety critical task scheduling systems in PPTL axiom system. J Comb Optim 31(2):1\u201327","journal-title":"J Comb Optim"}],"container-title":["Journal of Combinatorial Optimization"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-018-0343-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10878-018-0343-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-018-0343-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,2]],"date-time":"2019-09-02T19:15:39Z","timestamp":1567451739000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10878-018-0343-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,3]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,5]]}},"alternative-id":["343"],"URL":"https:\/\/doi.org\/10.1007\/s10878-018-0343-1","relation":{},"ISSN":["1382-6905","1573-2886"],"issn-type":[{"type":"print","value":"1382-6905"},{"type":"electronic","value":"1573-2886"}],"subject":[],"published":{"date-parts":[[2018,9,3]]},"assertion":[{"value":"3 September 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}