{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T01:19:26Z","timestamp":1773105566621,"version":"3.50.1"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,2,23]],"date-time":"2014-02-23T00:00:00Z","timestamp":1393113600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2014,6]]},"DOI":"10.1007\/s11227-014-1127-8","type":"journal-article","created":{"date-parts":[[2014,2,22]],"date-time":"2014-02-22T10:23:28Z","timestamp":1393064608000},"page":"1604-1629","source":"Crossref","is-referenced-by-count":6,"title":["Scheduling analysis based on model checking for multiprocessor real-time systems"],"prefix":"10.1007","volume":"68","author":[{"given":"Walid","family":"Karamti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adel","family":"Mahfoudhi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,2,23]]},"reference":[{"key":"1127_CR1","doi-asserted-by":"crossref","unstructured":"Amnell T, Fersman E, Mokrushin L, Pettersson P, Wang Y (2002) Times\u2014a tool for modelling and implementation of embedded systems. In: TACAS \u201902: Proceedings of the 8th international conference on tools and algorithms for the construction and analysis of systems. Springer, London, pp 460\u2013464","DOI":"10.1007\/3-540-46002-0_32"},{"key":"1127_CR2","unstructured":"Antti V (1989) Stubborn sets for reduced state space generation. In: Applications and theory of Petri Nets, pp 491\u2013515"},{"issue":"3","key":"1127_CR3","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":"1127_CR4","doi-asserted-by":"crossref","unstructured":"Berthomieu B, Peres F, Vernadat F (2006) Bridging the gap between timed automata and bounded time petri nets. In: FORMATS, pp 82\u201397","DOI":"10.1007\/11867340_7"},{"key":"1127_CR5","unstructured":"Berthomieu B, Vernadat F (2006) Time petri nets analysis with tina. In: QEST, pp 123\u2013124"},{"issue":"5","key":"1127_CR6","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1016\/j.sysarc.2010.09.004","volume":"57","author":"M Bertogna","year":"2011","unstructured":"Bertogna M, Baruah SK (2011) Tests for global EDF schedulability analysis. J Syst Archit Embed Syst Design 57(5):487\u2013497","journal-title":"J Syst Archit Embed Syst Design"},{"key":"1127_CR7","doi-asserted-by":"crossref","unstructured":"Buy U, Sloan RH (1994) Analysis of real-time programs with simple time petri nets. In: ISSTA \u201994: Proceedings of the 1994 ACM SIGSOFT international symposium on software testing and analysis. ACM, New York, pp 228\u2013239","DOI":"10.1145\/186258.187243"},{"key":"1127_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/3-540-63139-9_38","volume-title":"Application and theory of petri nets 1997","author":"F Bause","year":"1997","unstructured":"Bause F (1997) Analysis of petri nets with a dynamic priority method. In: Az\u00e9ma Pierre, Balbo Gianfranco (eds) Application and theory of petri nets 1997, vol 1248., Lecture Notes in Computer ScienceSpringer, Berlin, pp 215\u2013234"},{"key":"1127_CR9","unstructured":"Carpenter J, Funk S, Holman P, Srinivasan A, Anderson J, Baruah S (2004) A categorization of real-time multiprocessor scheduling problems and algorithms. In: Handbook on scheduling algorithms methods, and models. Chapman Hall\/CRC, Boca"},{"key":"1127_CR10","doi-asserted-by":"crossref","unstructured":"Gardey G, Lime D, Magnin M, Roux OH (2005) Romeo: a tool for analyzing time petri nets. In: CAV, pp 418\u2013423","DOI":"10.1007\/11513988_41"},{"key":"1127_CR11","doi-asserted-by":"crossref","unstructured":"Gonzalez Harbour M, Gutierrez Garciia JJ, Palencia Gutierrez JC, Drake Moyano JM (2001) Mast: modeling and analysis suite for real time applications. Euromicro conference on real-time systems, p 0125","DOI":"10.1109\/EMRTS.2001.934015"},{"key":"1127_CR12","unstructured":"Goossens J, Richard P; Universit\u00e9 Libre De Bruxelles (2004) Overview of real-time scheduling problems. In: Euro workshop on project management and scheduling"},{"key":"1127_CR13","unstructured":"Hadj Kacem Y, Karamti W, Mahfoudhi A, Abid M (2010) A petri net extension for schedulability analysis of real time embedded systems. In: PDPTA, pp 304\u2013314"},{"key":"1127_CR14","unstructured":"Karamti W, Mahfoudhi A, Hadj Kacem Y (2012) Hierarchical modeling with dynamic priority time petri nets for multiprocessor scheduling analysis. In: ESA, the 2012 international conference on embedded systems and applications, pp 114\u2013121"},{"key":"1127_CR15","doi-asserted-by":"crossref","unstructured":"Karamti W, Mahfoudhi A, Hadj Kacem Y (2012) Using dynamic priority time petri nets for scheduling analysis via earliest deadline first policy. In: ISPA, Madrid, pp 332\u2013339","DOI":"10.1109\/ISPA.2012.50"},{"key":"1127_CR16","unstructured":"Karamti W, Mahfoudhi A, Hadj Kacem Y, Abid M (2012) A formal method for scheduling analysis of a partitioned multiprocessor system: dynamic priority time petri nets. In: PECCS, Italy, pp 317\u2013326"},{"issue":"5","key":"1127_CR17","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1016\/j.sysarc.2011.01.002","volume":"57","author":"S Kato","year":"2011","unstructured":"Kato S, Yamasaki N (2011) Global edf-based scheduling with laxity-driven priority promotion. J Syst Archit Embed Syst Design 57(5):498\u2013517","journal-title":"J Syst Archit Embed Syst Design"},{"key":"1127_CR18","unstructured":"Kimmo V (1994) On combining the stubborn set method with the sleep set method. In: Valette R (ed) Application and theory of petri nets 1994: proceedings of 15th international conference, Zaragoza, volume 815 of Lecture Notes in Computer Science, Spain. Springer, Berlin, pp 548\u2013567"},{"key":"1127_CR19","unstructured":"Kwang SH, Leung JY-T (1988) On-line scheduling of real-time tasks. In: IEEE real-time systems symposium, pp 244\u2013250"},{"issue":"2","key":"1127_CR20","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/s11241-008-9059-0","volume":"41","author":"D Lime","year":"2009","unstructured":"Lime D, Roux OH (2009) Formal verification of real-time systems with preemptive scheduling. Real-Time Syst 41(2):118\u2013151","journal-title":"Real-Time Syst"},{"key":"1127_CR21","doi-asserted-by":"crossref","unstructured":"Lime D, Roux OH (2004) A translation based method for the timed analysis of scheduling extended time petri nets. In: RTSS \u201904: proceedings of the 25th IEEE international real-time systems symposium. IEEE Computer Society, Washington, DC, pp 187\u2013196","DOI":"10.1109\/REAL.2004.9"},{"key":"1127_CR22","doi-asserted-by":"crossref","unstructured":"Liu CL, Layland JW (1973) Scheduling algorithms for multiprogramming in a hard-real-time environment. J ACM 20:46\u201361","DOI":"10.1145\/321738.321743"},{"key":"1127_CR23","unstructured":"Object Management Group (OMG) (2008) A UML profile for MARTE: modeling and analysis of real-time embedded systems, beta 2, ptc\/2008-06-09. Object Management Group"},{"key":"1127_CR24","doi-asserted-by":"crossref","unstructured":"Sha L, Abdelzaher T, Arz\u00e9n KE, Cervin A, Baker T, Burns A, Buttazzo G, Caccamo M, Lehoczky J, Mok KA (2004) Real time scheduling theory: a historical perspective. Real Time Syst 28:101\u2013155","DOI":"10.1023\/B:TIME.0000045315.61234.1e"},{"issue":"3","key":"1127_CR25","doi-asserted-by":"crossref","first-page":"1478","DOI":"10.1007\/s11227-011-0557-9","volume":"59","author":"A Mahfoudhi","year":"2012","unstructured":"Mahfoudhi A, Hadj Y, Karamti KW, Abid M (2012) Compositional specification of real time embedded systems by priority time petri nets. J Supercomput 59(3):1478\u20131503","journal-title":"J Supercomput"},{"key":"1127_CR26","unstructured":"Merlin PM (1974) A study of the recoverability of computing systems. PhD Thesis, Univ. California, Irvine. Available from Univ Microfilms, Ann Arbor, No. 75-11026"},{"key":"1127_CR27","unstructured":"Petri CA (1962) Fundamentals of a theory of asynchronous information flow. In: IFIP congress, pp 386\u2013390"},{"issue":"7","key":"1127_CR28","first-page":"973","volume":"36","author":"OH Roux","year":"2002","unstructured":"Roux OH, D\u00e9planche AM (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":"1127_CR29","doi-asserted-by":"crossref","unstructured":"Schmidt DC (2006) Model-driven engineering. IEEE Comput 39(2)","DOI":"10.1109\/MC.2006.58"},{"key":"1127_CR30","doi-asserted-by":"crossref","unstructured":"Singhoff F, Legrand J, Nana LT, Marc\u00e9 L (2004) Cheddar: a flexible real time scheduling framework. ACM Ada Lett J 24(4):1\u20138. ACM Press, ISSN :1094-3641","DOI":"10.1145\/1032297.1032298"},{"issue":"11","key":"1127_CR31","doi-asserted-by":"crossref","first-page":"1208","DOI":"10.1016\/j.mejo.2006.07.028","volume":"37","author":"H Tmar","year":"2006","unstructured":"Tmar H, Diguet JP, Azzedine A, Abid M, Philippe JL (2006) Rtdt: a static qos manager, rt scheduling, hw\/sw partitioning cad tool. Microelectron J 37(11):1208\u20131219","journal-title":"Microelectron J"},{"issue":"3\u20134","key":"1127_CR32","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1016\/j.sysarc.2012.03.001","volume":"58","author":"F Trivi\u00f1o","year":"2012","unstructured":"Trivi\u00f1o F, S\u00e1nchez JL, Alfaro FJ, Flich J (2012) Network-on-chip virtualization in chip-multiprocessor systems. J Syst Archit Embed Syst Design 58(3\u20134):126\u2013139","journal-title":"J Syst Archit Embed Syst Design"},{"key":"1127_CR33","doi-asserted-by":"crossref","unstructured":"Veloso M, Pagello E, Kitano H (eds) (2000) Robocup-99: Robot Soccer World Cup III","DOI":"10.1007\/3-540-45327-X"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-014-1127-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11227-014-1127-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-014-1127-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T21:46:57Z","timestamp":1565214417000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11227-014-1127-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,23]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,6]]}},"alternative-id":["1127"],"URL":"https:\/\/doi.org\/10.1007\/s11227-014-1127-8","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"value":"0920-8542","type":"print"},{"value":"1573-0484","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2,23]]}}}