{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T06:58:45Z","timestamp":1648796325896},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,6,28]],"date-time":"2009-06-28T00:00:00Z","timestamp":1246147200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2009,9]]},"DOI":"10.1007\/s11334-009-0093-4","type":"journal-article","created":{"date-parts":[[2009,6,27]],"date-time":"2009-06-27T05:23:33Z","timestamp":1246080213000},"page":"163-179","source":"Crossref","is-referenced-by-count":0,"title":["Verification of real-time systems with preemption: negative and positive results"],"prefix":"10.1007","volume":"5","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Boniol","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00e9r\u00f4me","family":"Ermont","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claire","family":"Pagetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,6,28]]},"reference":[{"key":"93_CR1","unstructured":"Aceto L, Bouyer P, Burgue\u00f1o A, Larsen KG (2001) The power of reachability testing for timed automata. Tech. Rep. LSV-01-6, ENS Cachan, France"},{"key":"93_CR2","doi-asserted-by":"crossref","unstructured":"Ad\u00e9la\u00efde M, Roux O (2002) A class of decidable parametric hybrid systems. In: 9th International conference on algebraic methodology and software technology. Lecture Notes in Computer Science, vol 2422. Springer, Heidelberg","DOI":"10.1007\/3-540-45719-4_10"},{"issue":"2","key":"93_CR3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) Theory of timed automata. Theor Comp Sci 126(2): 183\u2013235","journal-title":"Theor Comp Sci"},{"key":"93_CR4","unstructured":"Alur R, Courcoubetis C, Henzinger TA, Ho PH (1992) Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Hybrid systems, pp 209\u2013229"},{"key":"93_CR5","doi-asserted-by":"crossref","unstructured":"B\u00e9rard B, Laroussinie F, Petit A, Schnoebelen P (2001) Systems and software verification. Model-checking techniques and tools. Springer, Heidelberg","DOI":"10.1007\/978-3-662-04558-9"},{"key":"93_CR6","doi-asserted-by":"crossref","unstructured":"Bozga M, Daws C, Maler O, Olivera A, Tripakis S, Yovine S (1998) KRONOS: A model-checking tool for real-time systems. In: Hu AJ, Vardi MY (eds) 10th International conference on computer aided verification, Springer, Vancouver, Canada, Lecture Notes in Computer Science, vol 1427, pp 546\u2013550","DOI":"10.1007\/BFb0028779"},{"key":"93_CR7","doi-asserted-by":"crossref","unstructured":"Cassez F, Larsen KG (2000) The impressive power of stopwatches. In: Palamidessi C (ed) CONCUR. Lecture Notes in Computer Science, vol 1877. Springer, Heidelberg, pp 138\u2013152","DOI":"10.1007\/3-540-44618-4_12"},{"key":"93_CR8","unstructured":"Cerans K (1992) Algorithmic problems in analysis of real-time systems specifications. Ph.D. thesis, Institut of Mathematical and Computer Science, University of Latvia, Riga"},{"key":"93_CR9","doi-asserted-by":"crossref","DOI":"10.1002\/0471224626","volume-title":"Real-time systems: scheduling, analysis, and verification","author":"AMK Cheng","year":"2002","unstructured":"Cheng AMK (2002) Real-time systems: scheduling, analysis, and verification. Wiley, New York"},{"key":"93_CR10","unstructured":"Ermont J (2002) Une alg\u00e8bre de processus pour la mod\u00e9lisation et la v\u00e9rification de syst\u00e8mes temps-r\u00e9el avec pr\u00e9emption. Ph.D. thesis, Ecole Nationale Sup\u00e9rieure de l\u2019A\u00e9ronautique et de l\u2019Espace, Toulouse"},{"key":"93_CR11","volume-title":"Electronic notes in theoretical computer science, vol 65","author":"J Ermont","year":"2002","unstructured":"Ermont J, Boniol F (2002) TPAP: an algebra of preemptive processes for verifying real-time systems with shared resources. In: Asarin E, Maler O, Yovine S (eds) Electronic notes in theoretical computer science, vol 65. Elsevier, Amsterdam"},{"key":"93_CR12","doi-asserted-by":"crossref","unstructured":"Fersman E, Krcal P, Pettersson P, Yi W (2007) Task automata: schedulability, decidability and undecidability. Int J Inform Comput","DOI":"10.1016\/j.ic.2007.01.009"},{"key":"93_CR13","doi-asserted-by":"crossref","unstructured":"Havelund K, Skou A, Larsen KG, Lund K (1997) Formal modelling and analysis of an audio\/video protocol: an industrial case study using Uppaal. In: Proceedings of the 18th IEEE real-time systems symposium, San Francisco, California, USA, pp 2\u201313","DOI":"10.1109\/REAL.1997.641264"},{"key":"93_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger T (1996) The theory of hybrid automata. In: Proceedings of the 11th annual IEEE symposium on logic in computer science (LICS \u201996), New Brunswick, New Jersey, pp 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"key":"93_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Nicollin X, Sifakis J, Yovine S (1992) Symbolic model checking for real-time systems. In: 7th. LiCS Symposium, Santa-Cruz, California, pp 394\u2013406","DOI":"10.1109\/LICS.1992.185551"},{"key":"93_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Ho PH, Wong-Toi H (1995) A user guide to HYTECH. In: Tools and algorithms for construction and analysis of systems, Springer, Lecture Notes in Computer Science, vol 1165, pp 41\u201347","DOI":"10.1007\/3-540-60630-0_3"},{"issue":"1\u20132","key":"93_CR17","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger TA, Ho PH, Wong-Toi H (1997) HYTECH: a model checker for hybrid systems. Int J Softw Tools Technol Transf 1(1\u20132): 110\u2013122","journal-title":"Int J Softw Tools Technol Transf"},{"key":"93_CR18","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger TA, Kopke PW, Puri A, Varaiya P (1998) What\u2019s decidable about hybrid automata? J Comp Syst Sci 57: 94\u2013124","journal-title":"J Comp Syst Sci"},{"issue":"3","key":"93_CR19","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(80)90123-4","volume":"11","author":"JMM Leung","year":"1980","unstructured":"Leung JMM (1980) A note on preemptive scheduling of periodic real-time tasks. Inform Process Lett 11(3): 115\u2013118","journal-title":"Inform Process Lett"},{"key":"93_CR20","doi-asserted-by":"crossref","unstructured":"Laroussinie F, Larsen KG (1998) CMC: a tool for compositional model-checking of real-time systems. In: Proc. IFIP joint int. conf. formal description techniques and protocol specification, testing, and verification (FORTE-PSTV\u201998), Kluwer, Paris, France, pp 439\u2013456","DOI":"10.1007\/978-0-387-35394-4_27"},{"key":"93_CR21","doi-asserted-by":"crossref","unstructured":"Laroussinie F, Larsen KG, Weise C (1995) From timed automata to logic\u2014and Back. In: MFCS95, Prague, Czech Republic","DOI":"10.7146\/brics.v2i2.19504"},{"issue":"1\u20132","key":"93_CR22","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1\u20132): 134\u2013152","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"2","key":"93_CR23","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0166-5316(82)90024-4","volume":"2","author":"JYT Leung","year":"1982","unstructured":"Leung JYT, Whitehead J (1982) On the complexity of fixed- priority scheduling of periodic real-time tasks. Perform Eval 2(2): 237\u2013250","journal-title":"Perform Eval"},{"key":"93_CR24","doi-asserted-by":"crossref","unstructured":"Liu CL, Layland JW (1973) Scheduling algorithms for multiprogramming in a hard-real-time environment. J ACM 20(1):46\u201361, http:\/\/citeseer.ist.psu.edu\/liu73scheduling.html","DOI":"10.1145\/321738.321743"},{"key":"93_CR25","volume-title":"Computation: finite and infinite machines","author":"M Minsky","year":"1967","unstructured":"Minsky M (1967) Computation: finite and infinite machines. Prentice-Hall, Englewood Cliffs"},{"key":"93_CR26","unstructured":"Pailler S (2006) Analyse hors ligne d\u2019ordonnan\u00e7abilit d\u2019applications temps rel comportant des t\u00e2ches conditionnelles et sporadiques. Ph.D. thesis, Universit\u00e9 de Poitiers"},{"key":"93_CR27","doi-asserted-by":"crossref","unstructured":"Puri A, Varaiya P (1995) Decidable hybrid systems. In: Hybrid systems II, Springer. Lecture Notes in Computer Science, vol 999, pp 359\u2013369","DOI":"10.1007\/3-540-60472-3_18"},{"key":"93_CR28","unstructured":"Rusu V (1996) V\u00e9rification temporelle de programmes Electre. Ph.D. thesis, Ecole Centrale de Nantes"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0093-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-009-0093-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0093-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T02:25:58Z","timestamp":1589941558000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-009-0093-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,28]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,9]]}},"alternative-id":["93"],"URL":"https:\/\/doi.org\/10.1007\/s11334-009-0093-4","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,6,28]]}}}