{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:51:02Z","timestamp":1762458662298},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,8,28]],"date-time":"2008-08-28T00:00:00Z","timestamp":1219881600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Real-Time Syst"],"published-print":{"date-parts":[[2009,2]]},"DOI":"10.1007\/s11241-008-9059-0","type":"journal-article","created":{"date-parts":[[2008,8,27]],"date-time":"2008-08-27T16:03:52Z","timestamp":1219853032000},"page":"118-151","source":"Crossref","is-referenced-by-count":29,"title":["Formal verification of real-time systems with\u00a0preemptive scheduling"],"prefix":"10.1007","volume":"41","author":[{"given":"Didier","family":"Lime","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier (H. )","family":"Roux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,8,28]]},"reference":[{"key":"9059_CR1","first-page":"154","volume-title":"20th IEEE real-time systems symposium","author":"K Altisen","year":"1999","unstructured":"Altisen K, G\u00f6ssler G, Pnueli A, Sifakis J, Tripakis S, Yovine S (1999) A framework for scheduler synthesis. In: 20th IEEE real-time systems symposium, RTSS\u201999, Phoenix, Arizona, USA. IEEE Computer Society Press, Washington, pp 154\u2013163"},{"key":"9059_CR2","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/3-540-45352-0_11","volume-title":"6th international symposium on formal techniques in real-time and fault-tolerant systems","author":"K Altisen","year":"2000","unstructured":"Altisen K, G\u00f6ssler G, Sifakis J (2000) A methodology for the construction of scheduled systems. In: 6th international symposium on formal techniques in real-time and fault-tolerant systems, FTRTFT\u201900, Pune. Lecture notes in computer science, vol 1926. Springer, New York, pp 106\u2013120"},{"key":"9059_CR3","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1023\/A:1015346419267","volume":"23","author":"K Altisen","year":"2002","unstructured":"Altisen K, G\u00f6ssler G, Sifakis J (2002) Scheduler modelling based on the controller synthesis paradigm. J\u00a0Real-Time Syst 23:55\u201384. Special issue on control-theoretical approaches to real-time computing","journal-title":"J\u00a0Real-Time Syst"},{"issue":"2","key":"9059_CR4","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) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"9059_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho P-H, Nicollin X, Olivero A, Sifakis J, Yovine S (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138:3\u201334","journal-title":"Theor Comput Sci"},{"key":"9059_CR6","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R Alur","year":"1996","unstructured":"Alur R, Henzinger TA, Ho P-H (1996) Automatic symbolic verification of embedded systems. IEEE Trans Softw Eng 22:181\u2013201","journal-title":"IEEE Trans Softw Eng"},{"key":"9059_CR7","volume-title":"Finite transition system","author":"A Arnold","year":"1994","unstructured":"Arnold A (1994) Finite transition system. Prentice-Hall, Englewood Cliffs"},{"key":"9059_CR8","doi-asserted-by":"crossref","unstructured":"Aura T, Lilius J (2000). A causal semantics for time Petri nets. Theor Comput Sci","DOI":"10.1016\/S0304-3975(99)00114-0"},{"key":"9059_CR9","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/978-3-540-45069-6_12","volume-title":"Proceedings of the 15th international conference on computer aided verification","author":"S Bardin","year":"2003","unstructured":"Bardin S, Finkel A, Leroux J, Petrucci L (2003) FAST: fast acceleration of symbolic transition systems. In: Proceedings of the 15th international conference on computer aided verification, CAV\u201903. Lecture notes in computer science, vol 2725. Springer, New York, pp 118\u2013121"},{"issue":"3","key":"9059_CR10","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B Berthomieu","year":"1991","unstructured":"Berthomieu B, Diaz M (1991) Modeling and verification of time dependent systems using time Petri nets. IEEE Trans Softw Eng 17(3):259\u2013273","journal-title":"IEEE Trans Softw Eng"},{"key":"9059_CR11","first-page":"41","volume":"9","author":"B Berthomieu","year":"1983","unstructured":"Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time Petri nets. IFIP Congress Ser 9:41\u201346","journal-title":"IFIP Congress Ser"},{"issue":"2","key":"9059_CR12","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s10626-006-0011-y","volume":"17","author":"B Berthomieu","year":"2007","unstructured":"Berthomieu B, Lime D, Roux OH, Vernadat F (2007) Reachability problems and abstract state spaces for time Petri nets with stopwatches. J Discrete Event Dyn Syst (jDEDS) 17(2):133\u2013158","journal-title":"J Discrete Event Dyn Syst (jDEDS)"},{"key":"9059_CR13","first-page":"417","volume-title":"4th international conference on concurrency theory","author":"P Br\u00e9mond-Gr\u00e9goire","year":"1993","unstructured":"Br\u00e9mond-Gr\u00e9goire P, Lee I, Gerber R (1993) Acsr: an algebra of communicating shared resources with dense time and priorities. In: 4th international conference on concurrency theory, CONCUR\u201993, London. Springer, New York, pp 417\u2013431"},{"key":"9059_CR14","doi-asserted-by":"crossref","unstructured":"Bucci G, Fedeli A, Sassoli L, Vicario E (2003). Modeling flexible real time systems with preemptive time Petri nets. In: 15th Euromicro conference on real-time systems, ECRTS\u20192003, pp 279\u2013286","DOI":"10.1109\/EMRTS.2003.1212753"},{"issue":"2","key":"9059_CR15","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1109\/TSE.2004.1265815","volume":"30","author":"G Bucci","year":"2004","unstructured":"Bucci G, Fedeli A, Sassoli L, Vicario E (2004) Time state space analysis of real-time preemptive systems. IEEE Trans Softw Eng 30(2):97\u2013111","journal-title":"IEEE Trans Softw Eng"},{"key":"9059_CR16","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/3-540-44618-4_12","volume-title":"11th international conference on concurrency theory","author":"F Cassez","year":"2000","unstructured":"Cassez F, Larsen KG (2000) The impressive power of stopwatches. In: Palamidesi C (ed) 11th international conference on concurrency theory, CONCUR\u20192000, University Park. Lecture notes in computer science, vol 1877. Springer, New York, pp 138\u2013152"},{"issue":"10","key":"9059_CR17","doi-asserted-by":"crossref","first-page":"1456","DOI":"10.1016\/j.jss.2005.12.021","volume":"79","author":"F Cassez","year":"2006","unstructured":"Cassez F, Roux OH (2006) Structural translation from time Petri nets to timed automata\u2014model-checking time petri nets via timed automata. J Syst Softw 79(10):1456\u20131468","journal-title":"J Syst Softw"},{"key":"9059_CR18","doi-asserted-by":"crossref","unstructured":"Dantzig GB (1963). Linear programming and extensions. IEICE Trans Inf Syst","DOI":"10.7249\/R366"},{"key":"9059_CR19","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1109\/REAL.1996.563702","volume-title":"1996 IEEE real-time systems symposium","author":"C Daws","year":"1996","unstructured":"Daws C, Yovine S (1996) Reducing the number of clock variables of timed automata. In: 1996 IEEE real-time systems symposium, RTSS\u201996. IEEE Computer Society Press, Washington, pp 73\u201381"},{"key":"9059_CR20","unstructured":"Dill DL (1989). Timing assumptions and verification of finite-state concurrent systems. In: Workshop automatic verification methods for finite-state systems, vol\u00a0407, pp 197\u2013212"},{"issue":"2","key":"9059_CR21","first-page":"129","volume":"11","author":"E Fersman","year":"2004","unstructured":"Fersman E, Yi W (2004) A generic approach to schedulability analysis of real time tasks. Nord J Comput 11(2):129\u2013147","journal-title":"Nord J Comput"},{"key":"9059_CR22","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-46002-0_6","volume-title":"8th international conference on tools and algorithms for the construction and analysis of systems","author":"E Fersman","year":"2002","unstructured":"Fersman E, Petterson P, Yi W (2002) Timed automata with asynchronous processes: schedulability and decidability. In: 8th international conference on tools and algorithms for the construction and analysis of systems, TACAS\u201902, Grenoble. Lecture notes in computer science, vol 2280. Springer, New York, pp 67\u201382"},{"key":"9059_CR23","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/3-540-36577-X_16","volume-title":"9th international conference on tools and algorithms for the construction and analysis of systems","author":"E Fersman","year":"2003","unstructured":"Fersman E, Mokrushin L, Pettersson P, Yi W (2003) Schedulability analysis using two clocks. In: Garavel H, Hatcliff J (eds) 9th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2003. Lecture notes in computer science, vol 2619. Springer, New York, pp 224\u2013239"},{"key":"9059_CR24","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/j.tcs.2005.11.019","volume":"354","author":"E Fersman","year":"2006","unstructured":"Fersman E, Mokrushin L, Pettersson P, Yi W (2006) Schedulability analysis of fixed-priority systems using timed automata. Theor Comput Sci 354:301\u2013317","journal-title":"Theor Comput Sci"},{"key":"9059_CR25","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/11513988_41","volume-title":"17th international conference on computer aided verification","author":"G Gardey","year":"2005","unstructured":"Gardey G, Lime D, Magnin M, Roux OH (2005) Rom\u00e9o: a tool for analyzing time Petri nets. In: Etessami K, Rajamani SK (eds) 17th international conference on computer aided verification, CAV 2005, Edinburgh. Lecture notes in computer science, vol 3576. Springer, New York, pp 418\u2013423"},{"issue":"3","key":"9059_CR26","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1017\/S147106840600264X","volume":"6","author":"G Gardey","year":"2006","unstructured":"Gardey G, Roux OH, Roux OF (2006) State space computation and analysis of time Petri nets. Theory Pract Log Program (TPLP) 6(3):301\u2013320. Special issue on specification analysis and verification of reactive systems","journal-title":"Theory Pract Log Program (TPLP)"},{"key":"9059_CR27","first-page":"116","volume-title":"12th IEEE real-time systems symposium","author":"MG Harbour","year":"1991","unstructured":"Harbour MG, Klein MH, Lehoczky JP (1991) Fixed priority scheduling of periodic tasks with varying execution priority. In: 12th IEEE real-time systems symposium, RTSS\u201991, San Antonio. IEEE Computer Society Press, Washington, pp 116\u2013128"},{"issue":"2","key":"9059_CR28","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger TA, Nicollin X, Sifakis J, Yovine S (1994) Symbolic model-checking for real-time systems. Inf Comput 111(2):193\u2013244","journal-title":"Inf Comput"},{"issue":"1\u20132","key":"9059_CR29","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger TA, Ho P-H, Wong-Toi H (1997) Hytech: a model-checker for hybrid systems. J Softw Tools Technol Transf 1(1\u20132):110\u2013122","journal-title":"J Softw Tools Technol Transf"},{"key":"9059_CR30","unstructured":"Hladik P-E, D\u00e9planche A-M (2003). Analyse d\u2019ordonnan\u00e7abilit\u00e9 de t\u00e2ches temps-r\u00e9el avec offset et gigue. In: 11th international conference on real-time systems, RTS\u201903, Paris, France"},{"key":"9059_CR31","doi-asserted-by":"crossref","unstructured":"Larsen KG, Pettersson P, Yi W (1995). Model-checking for real-time systems. In: Fundamentals of computation theory, pp 62\u201388","DOI":"10.1007\/3-540-60249-6_41"},{"key":"9059_CR32","volume-title":"5th IFAC international conference on fieldbus systems and their applications","author":"D Lime","year":"2003","unstructured":"Lime D, Roux OH (2003) Expressiveness and analysis of scheduling extended time Petri nets. In: 5th IFAC international conference on fieldbus systems and their applications, FET 2003, Aveiro. Elsevier, Amsterdam"},{"key":"9059_CR33","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1109\/REAL.2004.9","volume-title":"25th IEEE real-time systems symposium","author":"D Lime","year":"2004","unstructured":"Lime D, Roux OH (2004) A translation-based method for the timed analysis of scheduling extended time Petri nets. In: 25th IEEE real-time systems symposium, RTSS 2004, Lisbon. IEEE Computer Society Press, Washington, pp 187\u2013196"},{"issue":"2","key":"9059_CR34","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/s10626-006-8133-9","volume":"16","author":"D Lime","year":"2006","unstructured":"Lime D, Roux OH (2006a) Model-checking of time Petri nets using the state class timed automaton. J\u00a0Discrete Event Dyn Syst (jDEDS) 16(2):179\u2013205","journal-title":"J\u00a0Discrete Event Dyn Syst (jDEDS)"},{"issue":"3","key":"9059_CR35","first-page":"347","volume":"25","author":"D Lime","year":"2006","unstructured":"Lime D, Roux OH (2006b) V\u00e9rification formelle des syst\u00e8mes temps r\u00e9el avec ordonnancement pr\u00e9emptif. Tech Sci Inf (TSI) 25(3):347\u2013375","journal-title":"Tech Sci Inf (TSI)"},{"issue":"1","key":"9059_CR36","first-page":"44","volume":"20","author":"C Liu","year":"1973","unstructured":"Liu C, Layland JW (1973) Scheduling algorithms for multiprogramming in a hard real-time environment. J ACM 20(1):44\u201361","journal-title":"J ACM"},{"key":"9059_CR37","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"59","volume-title":"3rd international workshop on software model-checking","author":"M Magnin","year":"2005","unstructured":"Magnin M, Lime D, Roux OH (2005) An efficient method for computing the exact state-space of petri nets with stopwatches. In: 3rd international workshop on software model-checking, SoftMC 2005, Edinburgh, Scotland, UK. Electronic Notes in Theoretical Computer Science, vol 144. Elsevier, Amsterdam, pp 59\u201377"},{"key":"9059_CR38","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/3-540-58179-0_47","volume-title":"6th international conference on computer aided verification","author":"J McManis","year":"1994","unstructured":"McManis J, Varaiya P (1994) Suspension automata: a decidable class of hybrid automata. In: Dill DL (ed) 6th international conference on computer aided verification, CAV\u201994, Stanford, CA, USA. Lecture notes in computer science, vol 818. Springer, New York, pp 105\u2013117"},{"key":"9059_CR39","unstructured":"Merlin PM (1974). A study of the recoverability of computing systems. PhD thesis, Dep of Information and Computer Science, University of California, Irvine, CA"},{"issue":"3","key":"9059_CR40","first-page":"148","volume":"18","author":"Y Okawa","year":"1996","unstructured":"Okawa Y, Yoneda T (1996) Schedulability verification of real-time systems with extended time Petri nets. Int J Mini Microcomput 18(3):148\u2013156","journal-title":"Int J Mini Microcomput"},{"key":"9059_CR41","unstructured":"OSEK Group (2001). OSEK\/VDX specification. http:\/\/www.osek-vdx.org"},{"key":"9059_CR42","first-page":"26","volume-title":"19th IEEE real-time systems symposium","author":"JC Palencia","year":"1998","unstructured":"Palencia JC, Harbour MG (1998) Schedulability analysis for tasks with static and dynamic offsets. In: 19th IEEE real-time systems symposium, RTSS\u201998, Madrid, Spain. IEEE Computer Society Press, Washington, pp 26\u201337"},{"key":"9059_CR43","first-page":"328","volume-title":"20th IEEE real-time systems symposium","author":"JC Palencia","year":"1999","unstructured":"Palencia JC, Harbour MG (1999) Exploiting precedence relations in the scheduling analysis of distributed real-time systems. In: 20th IEEE real-time systems symposium, RTSS\u201999, Phoenix, USA. IEEE Computer Society Press, Washington, pp 328\u2013339"},{"issue":"7","key":"9059_CR44","first-page":"973","volume":"36","author":"OH Roux","year":"2002","unstructured":"Roux OH, D\u00e9planche A-M (2002) A t-time Petri net extension for real time-task scheduling modeling. Eur J Autom (JESA) 36(7):973\u2013987","journal-title":"Eur J Autom (JESA)"},{"key":"9059_CR45","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/978-3-540-27793-4_21","volume-title":"The 25th international conference on application and theory of Petri nets","author":"OH Roux","year":"2004","unstructured":"Roux OH, Lime D (2004) Time Petri nets with inhibitor hyperarcs. Formal semantics and state space computation. In: Cortadella J, Reisig W (eds) The 25th international conference on application and theory of Petri nets, ICATPN 2004, Bologna, Italy. Lecture notes in computer science, vol 3099. Springer, New York, pp 371\u2013390"},{"key":"9059_CR46","doi-asserted-by":"crossref","unstructured":"Tindell K (1994). Fixed priority scheduling of hard real-time systems. PhD thesis, Department of Computer Science, University of New York","DOI":"10.1093\/comjnl\/37.8.691"}],"container-title":["Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11241-008-9059-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11241-008-9059-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11241-008-9059-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T11:09:51Z","timestamp":1559387391000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11241-008-9059-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,8,28]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["9059"],"URL":"https:\/\/doi.org\/10.1007\/s11241-008-9059-0","relation":{},"ISSN":["0922-6443","1573-1383"],"issn-type":[{"value":"0922-6443","type":"print"},{"value":"1573-1383","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,8,28]]}}}