{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T20:10:01Z","timestamp":1773259801987,"version":"3.50.1"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,9,29]],"date-time":"2015-09-29T00:00:00Z","timestamp":1443484800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Embedded Systems"],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1186\/s13639-015-0020-8","type":"journal-article","created":{"date-parts":[[2015,9,29]],"date-time":"2015-09-29T02:01:34Z","timestamp":1443492094000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Symbolic execution and timed automata model checking for timing analysis of Java real-time systems"],"prefix":"10.1186","volume":"2015","author":[{"given":"Kasper S.","family":"Luckow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bent","family":"Thomsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,9,29]]},"reference":[{"key":"20_CR1","volume-title":"Real-time systems and programming languages: ADA 95, real-time Java, and real-time POSIX","author":"A Burns","year":"2009","unstructured":"A Burns, A Wellings, Real-time systems and programming languages: ADA 95, real-time Java, and real-time POSIX, 4th (Addison-Wesley Educational Publishers Inc., Boston, MA, USA, 2009)."},{"key":"20_CR2","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-16256-5_6","volume-title":"Software Technologies for Embedded and Ubiquitous Systems","author":"C Ballabriga","year":"2010","unstructured":"C Ballabriga, H Cass\u00e9, C Rochange, P Sainrat, in Software Technologies for Embedded and Ubiquitous Systems, ed. by S Min, R Pettit, P Puschner, and T Ungerer. OTAWA: an open toolbox for adaptive WCET analysis (SpringerBerlin, Heidelberg, 2010), pp. 35\u201346. doi: 10.1007\/978-3-642-16256-5_6"},{"issue":"1","key":"20_CR3","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.scico.2007.01.014","volume":"69","author":"X Li","year":"2007","unstructured":"X Li, Y Liang, T Mitra, A Roychoudhury, Chronos: a timing analyzer for embedded software. Sci. Comput. Program. 69(1), 56\u201367 (2007).","journal-title":"Sci. Comput. Program."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"A Colin, I Puaut, in Real-Time Systems, 13th Euromicro Conference On. A modular and retargetable framework for tree-based WCET analysis (IEEE, 2001), pp. 37\u201344.","DOI":"10.1109\/EMRTS.2001.933995"},{"key":"20_CR5","volume-title":"8th International Workshop on Worst-Case Execution Time Analysis (WCET\u201908), OpenAccess Series in Informatics (OASIcs)","author":"A Prantl","year":"2008","unstructured":"A Prantl, M Schordan, J Knoop, in 8th International Workshop on Worst-Case Execution Time Analysis (WCET\u201908), OpenAccess Series in Informatics (OASIcs), 8, ed. by R Kirner. TuBound - a conceptually new tool for worst-case execution time analysis (Schloss Dagstuhl\u2013Leibniz-Zentrum fuer InformatikDagstuhl, Germany, 2008). doi: 10.4230\/OASIcs.WCET.2008.1661 . also published in print by Austrian Computer Society (OCG) with ISBN 978-3-85403-237-3. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2008\/1661. Accessed 23 Sep 2015."},{"key":"20_CR6","unstructured":"MUR-TR Center, SWEET (SWEdish Execution Time tool). http:\/\/www.mrtc.mdh.se\/projects\/wcet\/sweet\/ . Accessed 23 Sep 2015."},{"key":"20_CR7","unstructured":"AE Dalsgaard, MC Olesen, M Toft, RR Hansen, KG Larsen, in 10th International Workshop on Worst-Case Execution Time Analysis. METAMOC: modular execution time analysis using model checking, (2010). doi: http:\/\/dx.doi.org\/10.4230\/OASIcs.WCET.2010.113 . http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2010\/2831. Accessed 23 Sep 2015."},{"key":"20_CR8","unstructured":"N Holsti, S Saarinen, in Space Syst. Finl. Ltd. Status of the Bound-T WCET tool, (2002), pp. 25\u201330. Euromicro."},{"key":"20_CR9","unstructured":"RapiTime, RapiTime WCET tool homepage. Website. http:\/\/www.rapitasystems.com . Accessed 23 Sep 2015."},{"key":"20_CR10","unstructured":"C Ferdinand, R Heckmann, B Franzen, in Proceedings of VVSS2007 - 3rd European Symposium on Verification and Validation of Software Systems, 23rd of March 2007, Eindhoven, ed. by P Groot. Static memory and timing analysis of embedded systems code, (2007). http:\/\/www-fp.cs.st-andrews.ac.uk\/embounded\/pubs\/papers\/VVSS07.pdf . Accessed 23 Sep 2015."},{"issue":"2","key":"20_CR11","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1145\/2500886","volume":"57","author":"R Wilhelm","year":"2014","unstructured":"R Wilhelm, D Grund, Computation takes time, but how much?Commun. ACM. 57(2), 94\u2013103 (2014). doi: http:\/\/dx.doi.org\/10.1145\/2500886","journal-title":"Commun. ACM"},{"key":"20_CR12","unstructured":"D Locke, BS Andersen, B Brosgol, M Fulton, T Henties, JJ Hunt, JO Nielsen, K Nilsen, M Schoeberl, J Tokar, J Vitek, A Wellings, Safety-Critical Java Technology Specification, Public Draft, (2013). Java Community Process http:\/\/www.jcp.org\/en\/jsr\/detail?id=302 . Accessed 23 Sep 2015."},{"issue":"1","key":"20_CR13","first-page":"5","volume":"7","author":"A Armbruster","year":"2007","unstructured":"A Armbruster, J Baker, A Cunei, C Flack, D Holmes, F Pizlo, E Pla, M Prochazka, J Vitek, A real-time Java virtual machine with applications in Avionics. ACM Trans. Embed. Comput. Syst. (TECS). 7(1), 5\u20131549 (2007). doi: http:\/\/dx.doi.org\/10.1145\/1324969.1324974","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"20_CR14","volume-title":"Java for cost effective embedded real-time software","author":"S Korsholm","year":"2012","unstructured":"S Korsholm, Java for cost effective embedded real-time software (Department of Computer Science, Aalborg University, 2012)."},{"key":"20_CR15","unstructured":"KS Luckow, SE Korsholm, B Thomsen, in Proceedings of the 23rd Nordic Workshop on Programming Theory. NWPT \u201911. Towards a real-time, WCET analysable JVM running in 256 kB of flash memory, (2011), pp. 68\u201388. www.mrtc.mdh.se\/nwpt2011\/nwpt11-proceedings.pdf . Accessed 23 Sep 2015."},{"key":"20_CR16","unstructured":"M Schoeberl, JOP: A Java Optimized Processor for Embedded Real-Time Systems, vol. ISBN 978-3-8364-8086-4 (VDM Verlag Dr. M\u00fcller, 2008). http:\/\/www.amazon.com\/JOP-Optimized-Processor-Embedded-Real-Time\/dp\/3836480867 . Accessed 23 Sep 2015."},{"key":"20_CR17","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1145\/1620405.1620421","volume-title":"Proceedings of the 7th International Workshop on Java Technologies for Real-Time and Embedded Systems. JTRES \u201909","author":"F Pizlo","year":"2009","unstructured":"F Pizlo, L Ziarek, J Vitek, in Proceedings of the 7th International Workshop on Java Technologies for Real-Time and Embedded Systems. JTRES \u201909. Real time Java on resource-constrained platforms with Fiji VM (ACMNew York, NY, USA, 2009), pp. 110\u20139. doi: http:\/\/dx.doi.org\/10.1145\/1620405.1620421 . http:\/\/doi.acm.org\/10.1145\/1620405.1620421. Accessed 23 Sep 2015."},{"key":"20_CR18","unstructured":"Aicas, JamaicaVM user manual: Java technology for critical embedded systems (2010)."},{"key":"20_CR19","unstructured":"Atego, Atego home (2013). http:\/\/atego.com\/ . Accessed 23 Sep 2015."},{"key":"20_CR20","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/2402676.2402699","volume-title":"Proceedings of the 2012 ACM Conference on High Integrity Language Technology. HILT \u201912","author":"K Nilsen","year":"2012","unstructured":"K Nilsen, in Proceedings of the 2012 ACM Conference on High Integrity Language Technology. HILT \u201912. Real-time Java in modernization of the aegis weapon system (ACMNew York, NY, USA, 2012), pp. 63\u201370. doi: 10.1145\/2402676.2402699 . http:\/\/doi.acm.org\/10.1145\/2402676.2402699. Accessed 23 Sep 2015."},{"key":"20_CR21","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/1288940.1288955","volume-title":"Proceedings of the 5th International Workshop on Java Technologies for Real-time and Embedded Systems. JTRES \u201907","author":"SG Robertz","year":"2007","unstructured":"SG Robertz, R Henriksson, K Nilsson, A Blomdell, I Tarasov, in Proceedings of the 5th International Workshop on Java Technologies for Real-time and Embedded Systems. JTRES \u201907. Using real-time Java for industrial robot control (ACMNew York, NY, USA, 2007), pp. 104\u2013110. doi: http:\/\/dx.doi.org\/10.1145\/1288940.1288955 . http:\/\/doi.acm.org\/10.1145\/1288940.1288955. Accessed 23 Sep 2015."},{"issue":"6","key":"20_CR22","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1002\/spe.968","volume":"40","author":"M Schoeberl","year":"2010","unstructured":"M Schoeberl, W Puffitsch, RU Pedersen, B Huber, Worst-case execution time analysis for a Java processor. Softw. Pract. Experience. 40(6), 507\u2013542 (2010). doi: 10.1002\/spe.968","journal-title":"Softw. Pract. Experience"},{"key":"20_CR23","unstructured":"T B\u00f8gholm, H Kragh-Hansen, P Olsen, B Thomsen, KG Larsen, Model-based schedulability analysis of safety critical hard real-time Java programs (2008). doi: 10.1145\/1434790.1434807 . http:\/\/doi.acm.org\/10.1145\/1434790.1434807. Accessed 23 Sep 2015."},{"key":"20_CR24","unstructured":"C Frost, CS Jensen, KS Luckow, B Thomsen. 9th International Workshop on Java Technologies for Real-Time and Embedded Systems, (2011). doi: 10.1145\/2043910.2043916 . http:\/\/doi.acm.org\/10.1145\/2043910.2043916. Accessed 23 Sep 2015."},{"key":"20_CR25","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/2512989.2512992","volume-title":"Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems. JTRES \u201913","author":"KS Luckow","year":"2013","unstructured":"KS Luckow, T B\u00f8gholm, B Thomsen, KG Larsen, in Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems. JTRES \u201913. TetaSARTS: a tool for modular timing analysis of safety critical Java systems (ACMNew York, NY, USA, 2013), pp. 11\u201320. doi: 10.1145\/2512989.2512992 . http:\/\/doi.acm.org\/10.1145\/2512989.2512992. Accessed 23 Sep 2015."},{"issue":"7","key":"20_CR26","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"JC King, Symbolic execution and program testing. Commun. ACM. 19(7), 385\u2013394 (1976).","journal-title":"Commun. ACM"},{"issue":"3","key":"20_CR27","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/TSE.1976.233817","volume":"2","author":"LA Clarke","year":"1976","unstructured":"LA Clarke, A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2(3), 215\u2013222 (1976).","journal-title":"IEEE Trans. Softw. Eng."},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"J Bengtsson, K Larsen, F Larsson, P Pettersson, W Yi, in Proceedings of the DIMACS\/SYCON Workshop on Hybrid Systems III : Verification and Control: Verification and Control. Uppaal \u2013 a tool suite for automatic verification of real-time systems (SpringerSecaucus, NJ, USA, 1996), pp. 232\u2013243. http:\/\/dl.acm.org\/citation.cfm?id=239587.239611 . Accessed 23 Sep 2015.","DOI":"10.1007\/BFb0020949"},{"issue":"3","key":"20_CR29","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/s10515-013-0122-2","volume":"20","author":"CS P\u0103s\u0103reanu","year":"2013","unstructured":"CS P\u0103s\u0103reanu, W Visser, D Bushnell, J Geldenhuys, P Mehlitz, N Rungta, Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Autom. Softw. Eng. 20(3), 391\u2013425 (2013). doi: http:\/\/dx.doi.org\/10.1007\/s10515-013-0122-2","journal-title":"Autom. Softw. Eng."},{"key":"20_CR30","unstructured":"JPF, Java PathFinder tool-set (2014). http:\/\/babelfish.arc.nasa.gov\/trac\/jpf . Accessed 23 Sep 2015."},{"key":"20_CR31","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS\u201903","author":"S Khurshid","year":"2003","unstructured":"S Khurshid, CS P\u0103s\u0103reanu, W Visser, in Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS\u201903. Generalized symbolic execution for model checking and testing (SpringerBerlin, Heidelberg, 2003), pp. 553\u2013568. http:\/\/dl.acm.org\/citation.cfm?id=1765871.1765924 . Accessed 23 Sep 2015."},{"key":"20_CR32","doi-asserted-by":"publisher","unstructured":"J Bengtsson, W Yi, in Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science, 3098, ed. by J Desel, W Reisig, and G Rozenberg. Timed automata: semantics, algorithms and tools (Springer, pp. 87\u2013124. doi: 10.1007\/978-3-540-27755-2_3 . http:\/\/dx.doi.org\/10.1007\/978-3-540-27755-2_3. Accessed 23 Sep 2015.","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"20_CR33","first-page":"456","volume-title":"Proceedings of the 32Nd Annual ACM\/IEEE Design Automation Conference. DAC \u201995","author":"Y-TS Li","year":"1995","unstructured":"Y-TS Li, S Malik, in Proceedings of the 32Nd Annual ACM\/IEEE Design Automation Conference. DAC \u201995. Performance analysis of embedded software using implicit path enumerationACMNew York, NY, USA, 1995), pp. 456\u2013461. doi: 10.1145\/217474.217570 . http:\/\/doi.acm.org\/10.1145\/217474.217570. Accessed 23 Sep 2015."},{"key":"20_CR34","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/RTSS.2006.12","volume-title":"Real-Time Systems Symposium, 2006. RTSS\u201906. 27th IEEE International","author":"J Gustafsson","year":"2006","unstructured":"J Gustafsson, A Ermedahl, C Sandberg, B Lisper, in Real-Time Systems Symposium, 2006. RTSS\u201906. 27th IEEE International. Automatic derivation of loop bounds and infeasible paths for wcet analysis using abstract execution (IEEE Computer SocietyWashington, DC, USA, 2006), pp. 57\u201366. doi: http:\/\/dx.doi.org\/10.1109\/RTSS.2006.12"},{"key":"20_CR35","unstructured":"J Gustafsson, A Betts, A Ermedahl, B Lisper, in Proceedings of the 10th International Workshop on Worst-Case Execution Time Analysis. The M\u00e4lardalen WCET benchmarks\u2014past, present and future, (2010). http:\/\/www.es.mdh.se\/publications\/1895- . Accessed 23 Sep 2015."},{"key":"20_CR36","volume-title":"6th International Workshop on Worst-Case Execution Time Analysis (WCET\u201906), OpenAccess Series in informatics (OASIcs)","author":"D Kebbal","year":"2006","unstructured":"D Kebbal, P Sainrat, in 6th International Workshop on Worst-Case Execution Time Analysis (WCET\u201906), OpenAccess Series in informatics (OASIcs), 4, ed. by F Mueller. Combining symbolic execution and path enumeration in worst-case execution time analysis (Schloss Dagstuhl\u2013Leibniz-Zentrum fuer InformatikDagstuhl, Germany, 2006). doi: http:\/\/dx.doi.org\/10.4230\/OASIcs.WCET.2006.675 . http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/675. Accessed 23 Sep 2015."},{"key":"20_CR37","first-page":"128","volume-title":"Proceedings of the Second International Conference on Verification and Evaluation of Computer and Communication Systems. VECoS\u201908","author":"B Benhamamouch","year":"2008","unstructured":"B Benhamamouch, B Monsuez, F V\u00e9drine, in Proceedings of the Second International Conference on Verification and Evaluation of Computer and Communication Systems. VECoS\u201908. Computing WCET using symbolic execution (British Computer SocietySwinton, UK, UK, 2008), pp. 128\u2013139. http:\/\/dl.acm.org\/citation.cfm?id=2227461.2227475 . Accessed 23 Sep 2015."},{"issue":"2-3","key":"20_CR38","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1023\/A:1008138407139","volume":"17","author":"T Lundqvist","year":"1999","unstructured":"T Lundqvist, P Stenstr\u00f6m, An integrated path and timing analysis method based on cycle-level symbolic execution. Real-Time Syst. 17(2-3), 183\u2013207 (1999). doi: http:\/\/dx.doi.org\/10.1023\/A:1008138407139","journal-title":"Real-Time Syst."},{"key":"20_CR39","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1145\/2516821.2516847","volume-title":"Proceedings of the 21st International Conference on Real-Time Networks and Systems. RTNS \u201913","author":"J Knoop","year":"2013","unstructured":"J Knoop, L Kov\u00e1cs, J Zwirchmayr, in Proceedings of the 21st International Conference on Real-Time Networks and Systems. RTNS \u201913. WCET squeezing: on-demand feasibility refinement for proven precise wcet-bounds (ACMNew York, NY, USA, 2013), pp. 161\u201370. doi: 10.1145\/2516821.2516847 . http:\/\/doi.acm.org\/10.1145\/2516821.2516847. Accessed 23 Sep 2015."},{"key":"20_CR40","doi-asserted-by":"publisher","unstructured":"J Knoop, L Kov\u00e1cs, J Zwirchmayr, in Logic for Programming, Artificial Intelligence, and Reasoning. r-TuBound: Loop bounds for WCET analysis (Springer, 2012), pp. 435\u2013444.","DOI":"10.1007\/978-3-642-28717-6_34"},{"key":"20_CR41","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/11562948_33","volume-title":"Proceedings of the Third International Conference on Automated Technology for Verification and Analysis. ATVA\u201905","author":"G Lindstrom","year":"2005","unstructured":"G Lindstrom, PC Mehlitz, W Visser, in Proceedings of the Third International Conference on Automated Technology for Verification and Analysis. ATVA\u201905. Model checking real time Java using Java Pathfinder (SpringerBerlin, Heidelberg, 2005), pp. 444\u201356. doi: http:\/\/dx.doi.org\/10.1007\/11562948_33 . http:\/\/dx.doi.org\/10.1007\/11562948_33. Accessed 23 Sep 2015."},{"key":"20_CR42","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1145\/1850771.1850794","volume-title":"Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems. JTRES \u201910","author":"T Kalibera","year":"2010","unstructured":"T Kalibera, P Parizek, M Malohlava, M Schoeberl, in Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems. JTRES \u201910. Exhaustive testing of safety critical java (ACMNew York, NY, USA, 2010), pp. 164\u201374. doi: http:\/\/dx.doi.org\/10.1145\/1850771.1850794 . http:\/\/doi.acm.org\/10.1145\/1850771.1850794. Accessed 23 Sep 2015."},{"key":"20_CR43","unstructured":"T Amnell, E Fersman, L Mokrushin, P Pettersson, W Yi, in the 1st International Workshop on Formal Modeling and Analysis of Timed Systems. Times: a tool for schedulability analysis and code generation of real-time systems, (2003). http:\/\/www.es.mdh.se\/publications\/2047- . Accessed 23 Sep 2015."},{"key":"20_CR44","unstructured":"KS Luckow, T B\u00f8gholm, B Thomsen, in WiP Proceedings of the 19th Real-Time and Embedded Technology and Application Symposium. Supporting development of energy-optimised Java real-time systems using TetaSARTS, (2013), pp. 41\u20134. http:\/\/www.cister.isep.ipp.pt\/rtas2013\/WiP_Proceedings.pdf . Accessed 23 Sep 2015."},{"key":"20_CR45","unstructured":"DF Bacon, PF Sweeney, in Proceedings of the 11th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications. Fast static analysis of C++ virtual function calls. doi: 10.1145\/236337.236371 . http:\/\/doi.acm.org\/10.1145\/236337.236371. Accessed 23 Sep 2015."},{"issue":"1","key":"20_CR46","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2557833.2560571","volume":"39","author":"KS Luckow","year":"2014","unstructured":"KS Luckow, C P\u0103s\u0103reanu, Symbolic pathfinder v7. SIGSOFT Softw. Eng. Notes. 39(1), 1\u20135 (2014). doi: 10.1145\/2557833.2560571","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"20_CR47","doi-asserted-by":"crossref","unstructured":"KS Luckow, B Thomsen, SE Korsholm, in 12th International Workshop on Java Technologies for Real-Time and Embedded Systems. HVM-TP: a time predictable and portable Java virtual machine for hard real-time embedded systems (ACMNew York, 2014). To appear doi: http:\/\/doi.acm.org\/10.1145\/2661020.2661022","DOI":"10.1145\/2661020.2661022"},{"key":"20_CR48","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/2388936.2388945","volume-title":"Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems. JTRES \u201912","author":"H S\u00f8ndergaard","year":"2012","unstructured":"H S\u00f8ndergaard, SE Korsholm, AP Ravn, in Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems. JTRES \u201912. Safety-critical Java for low-end embedded platforms (ACMNew York, NY, USA, 2012), pp. 44\u201353. doi: 10.1145\/2388936.2388945 . http:\/\/doi.acm.org\/10.1145\/2388936.2388945. Accessed 23 Sep 2015."},{"key":"20_CR49","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-642-36742-7_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","author":"D Balasubramanian","year":"2013","unstructured":"D Balasubramanian, C P\u0103s\u0103reanu, G Karsai, M Lowry, in Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, 7795, ed. by N Piterman, S Smolka. Polyglot: systematic analysis for multiple statechart formalisms (SpringerBerlin, Heidelberg, 2013), pp. 523\u2013529. doi: http:\/\/dx.doi.org\/10.1007\/978-3-642-36742-7_36"},{"key":"20_CR50","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1145\/1850771.1850789","volume-title":"Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES \u201910","author":"M Schoeberl","year":"2010","unstructured":"M Schoeberl, TB Preusser, S Uhrig, in Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES \u201910. The embedded Java benchmark suite JemBench (ACMNew York, NY, USA, 2010), pp. 120\u20137. doi: 10.1145\/1850771.1850789 . http:\/\/doi.acm.org\/10.1145\/1850771.1850789. Accessed 23 Sep 2015."},{"key":"20_CR51","doi-asserted-by":"publisher","unstructured":"AE Dalsgaard, RR Hansen, KY J\u00f8rgensen, KG Larsen, MC Olesen, P Olsen, J Srba, K Havelund, G Holzmann, R Joshi, in NASA Formal Methods. Lecture Notes in Computer Science, 6617, ed. by M Bobaru. opaal: a lattice model checker, pp. 487\u201393. Springer. doi: http:\/\/dx.doi.org\/10.1007\/978-3-642-20398-5_37 . http:\/\/dx.doi.org\/10.1007\/978-3-642-20398-5_37. Accessed 23 Sep 2015.","DOI":"10.1007\/978-3-642-20398-5_37"},{"key":"20_CR52","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-33365-1_8","volume-title":"Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems","author":"AE Dalsgaard","year":"2012","unstructured":"AE Dalsgaard, A Laarman, KG Larsen, MC Olesen, J Van De Pol, in Proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems. Multi-core reachability for timed automata (Springer-VerlagBerlin, Heidelberg, 2012), pp. 91\u2013106. doi: 10.1007\/978-3-642-33365-1_8"}],"container-title":["EURASIP Journal on Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13639-015-0020-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1186\/s13639-015-0020-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13639-015-0020-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/s13639-015-0020-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T21:07:47Z","timestamp":1748639267000},"score":1,"resource":{"primary":{"URL":"https:\/\/jes-eurasipjournals.springeropen.com\/articles\/10.1186\/s13639-015-0020-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,29]]},"references-count":52,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,12]]}},"alternative-id":["20"],"URL":"https:\/\/doi.org\/10.1186\/s13639-015-0020-8","relation":{},"ISSN":["1687-3963"],"issn-type":[{"value":"1687-3963","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,29]]},"article-number":"2"}}