{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T10:49:17Z","timestamp":1790765357006,"version":"4.1.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,12,20]],"date-time":"2022-12-20T00:00:00Z","timestamp":1671494400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,20]],"date-time":"2022-12-20T00:00:00Z","timestamp":1671494400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2023,3]]},"DOI":"10.1007\/s10626-022-00372-6","type":"journal-article","created":{"date-parts":[[2022,12,20]],"date-time":"2022-12-20T09:07:32Z","timestamp":1671527252000},"page":"63-93","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Cost-optimal timed trace synthesis for scheduling of intermittent embedded systems"],"prefix":"10.1007","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7912-5161","authenticated-orcid":false,"given":"Antoine","family":"Bernabeu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Luc","family":"B\u00e9chennec","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mikael","family":"Briday","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastien","family":"Faucou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olivier","family":"Roux","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,12,20]]},"reference":[{"key":"372_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla PA, Mayr R (2013) Priced timed petri nets. Logical Methods in Computer Science 9(4). https:\/\/doi.org\/10.2168\/LMCS-9(4:10)2013","DOI":"10.2168\/LMCS-9(4:10)2013"},{"issue":"3","key":"372_CR2","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/j.tcs.2003.10.038","volume":"318","author":"R Alur","year":"2004","unstructured":"Alur R, Torre SL, Pappas GJ (2004) Optimal paths in weighted timed automata. Theoret Comput Sci 318(3):297\u2013322.","journal-title":"Theoret Comput Sci"},{"key":"372_CR3","doi-asserted-by":"publisher","unstructured":"Balsamo D et al (2015) Hibernus: sustaining computation during intermittent supply for energy-harvesting systems. IEEE Embed. Syst. Letters 7(1). https:\/\/doi.org\/10.1109\/LES.2014.2371494","DOI":"10.1109\/LES.2014.2371494"},{"key":"372_CR4","doi-asserted-by":"publisher","unstructured":"Balsamo D et al (2016) Hibernus++: a self-calibrating and adaptive system for transiently-powered embedded devices. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. 35(12). https:\/\/doi.org\/10.1109\/TCAD.2016.2547919","DOI":"10.1109\/TCAD.2016.2547919"},{"key":"372_CR5","first-page":"147","volume-title":"Minimum-Cost Reachability for Priced Timed Automata","author":"G Behrmann","year":"2001","unstructured":"Behrmann G et al (2001) Minimum-Cost Reachability for Priced Timed Automata. Springer, Berlin, pp 147\u2013161"},{"issue":"4","key":"372_CR6","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/1059816.1059823","volume":"32","author":"G Behrmann","year":"2005","unstructured":"Behrmann G, Larsen KG, Rasmussen JI (2005) Optimal scheduling using priced timed automata. SIGMETRICS Perform. Eval. Rev. 32(4):34\u201340. https:\/\/doi.org\/10.1145\/1059816.1059823","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"key":"372_CR7","doi-asserted-by":"crossref","unstructured":"Berthou G, Dagand P, Demange D, Oudin R, Risset T (2020) Intermittent computing with peripherals, formally verified","DOI":"10.1145\/3372799.3394365"},{"key":"372_CR8","doi-asserted-by":"crossref","unstructured":"Berthou G, Delizy T, Marquet K, Risset T, Salagnac G (2019) Sytare: a lightweight kernel for nvram-based transiently-powered systems. IEEE Trans. Comput 68(9)","DOI":"10.1109\/TC.2018.2889080"},{"key":"372_CR9","doi-asserted-by":"crossref","unstructured":"Berthou G, Marquet K, Risset T, Salagnac G (2020) Accurate power consumption evaluation for peripherals in ultra low-power embedded systems","DOI":"10.1109\/GIOTS49054.2020.9119593"},{"issue":"3","key":"372_CR10","doi-asserted-by":"publisher","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 Software Eng 17(3):259\u2013273","journal-title":"IEEE Trans Software Eng"},{"key":"372_CR11","unstructured":"Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time petri nets 41\u201346"},{"key":"372_CR12","volume-title":"Optimal reachability in cost time Petri nets. In: Nestmann, U, Wolter, K (eds) 15th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2017), Vol. 10419 of Lecture Notes in Computer Science","year":"2017","unstructured":"Boucheneb H, Lime D, Parquier B, Roux OH, Seidner C, Nestmann U, Wolter K (eds) (2017) Optimal reachability in cost time Petri nets. In: Nestmann, U, Wolter, K (eds) 15th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2017), Vol. 10419 of Lecture Notes in Computer Science. Springer, Berlin"},{"issue":"2","key":"372_CR13","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/3131848","volume":"23","author":"J Boukhobza","year":"2018","unstructured":"Boukhobza J, Rubini S, Chen R, Shao Z (2018) Emerging NVM: a survey on architectural integration and research challenges. ACM Trans Design Autom Electr Syst 23(2):14:1\u201314:32. https:\/\/doi.org\/10.1145\/3131848","journal-title":"ACM Trans Design Autom Electr Syst"},{"key":"372_CR14","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/j.peva.2013.11.002","volume":"73","author":"P Bouyer","year":"2014","unstructured":"Bouyer P, Larsen KG, Markey N (2014) Lower-bound-constrained runs in weighted timed automata. Perf Evaluation 73:91\u2013109. Special Issue on the 9th International Conference on Quantitative Evaluation of Systems","journal-title":"Perf Evaluation"},{"key":"372_CR15","doi-asserted-by":"crossref","unstructured":"Cammarano A, Petrioli C, Spenza D (2016) Online energy harvesting prediction in environmentally powered wireless sensor networks. IEEE Sensors Journal 16(17)","DOI":"10.1109\/JSEN.2016.2587220"},{"key":"372_CR16","doi-asserted-by":"crossref","unstructured":"Colin A, Lucia B (2018) Termination checking and task decomposition for task-based intermittent programs","DOI":"10.1145\/3178372.3179525"},{"key":"372_CR17","doi-asserted-by":"crossref","unstructured":"Dezfouli B, Amirtharaj I, Li C (2018) EMPIOT: an energy measurement platform for wireless iot devices. CoRR abs\/1804.04794","DOI":"10.1016\/j.jnca.2018.07.016"},{"issue":"2","key":"372_CR18","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01232184","volume":"2","author":"JR Haritsa","year":"1993","unstructured":"Haritsa JR, Carey MJ, Livny M (1993) Value-based scheduling in real-time database systems. VLDB J 2(2):117\u2013152. http:\/\/www.vldb.org\/journal\/VLDBJ2\/P117.pdf","journal-title":"VLDB J"},{"issue":"2","key":"372_CR19","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"4","author":"PE Hart","year":"1968","unstructured":"Hart PE, Nilsson NJ, Raphael B (1968) A formal basis for the heuristic determination of minimum cost paths. IEEE Transactions on Systems Science and Cybernetics 4(2):100\u2013107. https:\/\/doi.org\/10.1109\/TSSC.1968.300136. Conference Name: IEEE Transactions on Systems Science and Cybernetics","journal-title":"IEEE Transactions on Systems Science and Cybernetics"},{"issue":"3","key":"372_CR20","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/s00224-013-9449-0","volume":"54","author":"N Jain","year":"2014","unstructured":"Jain N, Menache I, Naor J, Yaniv J (2014) A truthful mechanism for value-based scheduling in cloud computing. Theory Comput Syst 54 (3):388\u2013406. https:\/\/doi.org\/10.1007\/s00224-013-9449-0","journal-title":"Theory Comput Syst"},{"key":"372_CR21","doi-asserted-by":"crossref","unstructured":"Kansal A, Hsu J, Zahedi S, Srivastava MB (2007) Power management in energy harvesting sensor networks. ACM Trans. Embed. Comput. Syst. 6(4)","DOI":"10.1145\/1274858.1274870"},{"key":"372_CR22","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume":"2102","author":"K Larsen","year":"2001","unstructured":"Larsen K, et al. (2001) As cheap as possible: efficient cost-optimal reachability for priced timed automata. Lect Notes Comput Sci 2102:493\u2013505","journal-title":"Lect Notes Comput Sci"},{"issue":"1-2","key":"372_CR23","first-page":"97","volume":"183","author":"D Lime","year":"2021","unstructured":"Lime D, Roux OH, Seidner C (2021) Cost problems for parametric time petri nets. Fund Inform 183(1-2):97\u2013123","journal-title":"Fund Inform"},{"key":"372_CR24","doi-asserted-by":"crossref","unstructured":"Lime D, Roux OH, Seidner C, Traonouez L-M, Kowalewski S, Philippou A (eds) (2009) Romeo: a parametric model-checker for Petri nets with stopwatches. In: Kowalewski, S, Philippou, A (eds). 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), Vol. 5505 of Lecture Notes in Computer Science. Springer, United Kingdom","DOI":"10.1007\/978-3-642-00768-2_6"},{"key":"372_CR25","doi-asserted-by":"publisher","unstructured":"Maeng K, Colin A, Lucia B (2017) Alpaca: intermittent execution without checkpoints. Proc. ACM Program. Lang. 1. https:\/\/doi.org\/10.1145\/3133920","DOI":"10.1145\/3133920"},{"key":"372_CR26","doi-asserted-by":"crossref","unstructured":"Maeng K, Lucia B (2020) Adaptive low-overhead scheduling for periodic and reactive intermittent execution, PLDI 2020 1005\u20131021 (Association for Computing Machinery)","DOI":"10.1145\/3385412.3385998"},{"key":"372_CR27","unstructured":"Merlin PM (1974) A study of the recoverability of computing systems. Ph.D. thesis, Department of Information and Computer Science, University of California, CA"},{"issue":"3","key":"372_CR28","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1017\/S0263574799002349","volume":"18","author":"D Prasad","year":"2000","unstructured":"Prasad D, Burns A (2000) A value-based scheduling approach for real-time autonomous vehicle control. Robotica 18(3):273\u2013279. https:\/\/doi.org\/10.1017\/S0263574799002349","journal-title":"Robotica"},{"key":"372_CR29","doi-asserted-by":"crossref","unstructured":"Ransford B, Sorber J, Fu K (2011) Mementos: system support for long-running computation on rfid-scale devices, ASPLOS XVI 159\u2013170 (Association for Computing Machinery)","DOI":"10.1145\/1961296.1950386"},{"issue":"1","key":"372_CR30","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10703-006-0014-1","volume":"29","author":"JI Rasmussen","year":"2006","unstructured":"Rasmussen JI, Larsen KG, Subramani K (2006) On using priced timed automata to achieve optimal scheduling. Formal Methods in System Design 29(1):97\u2013114","journal-title":"Formal Methods in System Design"},{"key":"372_CR31","doi-asserted-by":"crossref","unstructured":"Ruppel E, Lucia B (2019) Transactional concurrency control for intermittent energy-harvesting computing systems","DOI":"10.1145\/3314221.3314583"},{"key":"372_CR32","doi-asserted-by":"publisher","unstructured":"Surbatovich M, Lucia B, Jia L (2020) Towards a formal foundation of intermittent computing. Proc. ACM Program. Lang. 4(OOPSLA). https:\/\/doi.org\/10.1145\/3428231","DOI":"10.1145\/3428231"},{"key":"372_CR33","doi-asserted-by":"crossref","unstructured":"Sliper ST, Wang W, Nikoleris N, Weddell AS, Merrett GV (2020) Fused: closed-loop performance and energy simulation of embedded systems 263\u2013272","DOI":"10.1109\/ISPASS48437.2020.00046"},{"key":"372_CR34","unstructured":"W\u00e4gemann P, Dietrich C, Distler T, Ulbrich P, Schr\u00f6der-Preikschat W (2018) Whole-system worst-case energy-consumption analysis for energy-constrained real-time systems. Vol. 106"},{"key":"372_CR35","doi-asserted-by":"crossref","unstructured":"Yarahmadi B, Rohou E (2020) Compiler Optimizations for Safe Insertion of Checkpoints in Intermittently Powered Systems. https:\/\/hal.inria.fr\/hal-02914953","DOI":"10.1007\/978-3-030-60939-9_12"},{"key":"372_CR36","doi-asserted-by":"crossref","unstructured":"Y\u0131ld\u0131r\u0131m KS, et al. (2018) InK: reactive kernel for tiny batteryless sensors","DOI":"10.1145\/3274783.3274837"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-022-00372-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-022-00372-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-022-00372-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,3]],"date-time":"2023-03-03T11:19:39Z","timestamp":1677842379000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-022-00372-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,20]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["372"],"URL":"https:\/\/doi.org\/10.1007\/s10626-022-00372-6","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12,20]]},"assertion":[{"value":"16 March 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 November 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 December 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of Interests"}}]}}