{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T12:15:03Z","timestamp":1725884103469},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319572871"},{"type":"electronic","value":"9783319572888"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57288-8_8","type":"book-chapter","created":{"date-parts":[[2017,4,8]],"date-time":"2017-04-08T02:45:05Z","timestamp":1491619505000},"page":"115-130","source":"Crossref","is-referenced-by-count":8,"title":["Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets"],"prefix":"10.1007","author":[{"given":"Matteo","family":"Camilli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrizia","family":"Scandurra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo","family":"Bellettini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,9]]},"reference":[{"issue":"12","key":"8_CR1","doi-asserted-by":"crossref","first-page":"859","DOI":"10.1109\/TSE.2004.91","volume":"30","author":"N Delgado","year":"2004","unstructured":"Delgado, N., Gates, A.Q., Roach, S.: A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans. Softw. Eng. 30(12), 859\u2013872 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR2","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1109\/32.67597","volume":"17","author":"C Ghezzi","year":"1991","unstructured":"Ghezzi, C., Mandrioli, D., Morasca, S., Pezz\u00e8, M.: A unified high-level Petri net formalism for time-critical systems. IEEE Trans. Softw. Eng. 17, 160\u2013172 (1991)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-540-30482-1_31","volume-title":"Formal Methods and Software Engineering","author":"F Chen","year":"2004","unstructured":"Chen, F., D\u2019Amorim, M., Ro\u015fu, G.: A formal monitoring-based framework for software development and analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 357\u2013372. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30482-1_31"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Combining model-based testing and runtime monitoring for program testing in the presence of nondeterminism. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp. 178\u2013187, March 2013","DOI":"10.1109\/ICSTW.2013.29"},{"issue":"4","key":"8_CR5","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/s11334-009-0096-1","volume":"5","author":"H Liang","year":"2009","unstructured":"Liang, H., Dong, J.S., Sun, J., Wong, W.E.: Software monitoring through formal specification animation. Innov. Syst. Softw. Eng. 5(4), 231\u2013241 (2009)","journal-title":"Innov. Syst. Softw. Eng."},{"issue":"12","key":"8_CR6","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/S0304-3975(97)00078-9","volume":"202","author":"M Felder","year":"1998","unstructured":"Felder, M., Gargantini, A., Morzenti, A.: A theory of implementation and refinement in timed Petri nets. Theoret. Comput. Sci. 202(12), 127\u2013161 (1998)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR7","volume-title":"Timed Automata: Semantics, Algorithms and Tools","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. Springer, Heidelberg (2004)"},{"issue":"1","key":"8_CR8","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/343369.343384","volume":"1","author":"Y Gurevich","year":"2000","unstructured":"Gurevich, Y.: Sequential abstract-state machines capture sequential algorithms. ACM Trans. Comput. Log. 1(1), 77\u2013111 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"8_CR9","unstructured":"Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. Technical report, Cambridge, MA, USA (1974)"},{"issue":"3","key":"8_CR10","first-page":"15:1","volume":"10","author":"DGDL Iglesia","year":"2015","unstructured":"Iglesia, D.G.D.L., Weyns, D.: MAPE-K formal templates to rigorously design behaviors for self-adaptive systems. ACM Trans. Auton. Adapt. Syst. 10(3), 15:1\u201315:31 (2015)","journal-title":"ACM Trans. Auton. Adapt. Syst."},{"issue":"12","key":"8_CR11","doi-asserted-by":"crossref","first-page":"1115","DOI":"10.1109\/32.738342","volume":"24","author":"WJ Lee","year":"1998","unstructured":"Lee, W.J., Cha, S.D., Kwon, Y.R.: Integration and analysis of use cases using modular Petri nets in requirements engineering. IEEE Trans. Softw. Eng. 24(12), 1115\u20131130 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Zhu, H., Dwyer, M.B., Goddard, S.: Predictable runtime monitoring. In: Proceedings of the 2009 21st Euromicro Conference on Real-Time Systems, ser. ECRTS 2009, pp. 173\u2013183. IEEE Computer Society, Washington, DC (2011)","DOI":"10.1109\/ECRTS.2009.23"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/3-540-65306-6_21","volume-title":"Lectures on Petri Nets I: Basic Models","author":"A Valmari","year":"1998","unstructured":"Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429\u2013528. Springer, Heidelberg (1998). doi: 10.1007\/3-540-65306-6_21"},{"key":"8_CR14","volume-title":"Designing Concurrent, Distributed, and Real-Time Applications with UML","author":"H Gomaa","year":"2000","unstructured":"Gomaa, H.: Designing Concurrent, Distributed, and Real-Time Applications with UML, 1st edn. Addison-Wesley Longman Publishing Co., Inc., Boston (2000)","edition":"1"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Camilli, M., Gargantini, A., Scandurra, P.: Specifying and verifying real-time self-adaptive systems. In: 2015 IEEE 26th International Symposium on Software Reliability Engineering (ISSRE), pp. 303\u2013313, November 2015","DOI":"10.1109\/ISSRE.2015.7381823"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Bellettini, C., Capra, L.: Reachability analysis of time basic Petri nets: a time coverage approach. In: Proceedings of the 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, ser. SYNASC 2011, pp. 110\u2013117. IEEE Computer Society, Washington, DC (2011)","DOI":"10.1109\/SYNASC.2011.16"},{"key":"8_CR17","unstructured":"Maharaja framework. http:\/\/camilli.di.unimi.it\/maharaja\/ . Accessed Dec 2016"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-642-13675-7_20","volume-title":"Applications and Theory of Petri Nets","author":"LM Hillah","year":"2010","unstructured":"Hillah, L.M., Kordon, F., Petrucci, L., Tr\u00e8ves, N.: PNML framework: an extendable reference implementation of the Petri net markup language. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 318\u2013327. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-13675-7_20"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-45337-7_18","volume-title":"ECOOP 2001 \u2014 Object-Oriented Programming","author":"G Kiczales","year":"2001","unstructured":"Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327\u2013354. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45337-7_18"},{"key":"8_CR20","unstructured":"Chronicle Software: Java Thread Affinity Library (2016). http:\/\/chronicle.software\/products\/thread-affinity\/ . Accessed Jan 2016"},{"issue":"4","key":"8_CR21","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1145\/1594835.1504188","volume":"44","author":"T Li","year":"2009","unstructured":"Li, T., Baumberger, D., Hahn, S.: Efficient and scalable multiprocessor fair scheduling using distributed weighted round-robin. SIGPLAN Not. 44(4), 65\u201374 (2009)","journal-title":"SIGPLAN Not."},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-642-29860-8_17","volume-title":"Runtime Verification","author":"P Arcaini","year":"2012","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: CoMA: conformance monitoring of Java programs by abstract state machines. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 223\u2013238. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-29860-8_17"},{"issue":"2","key":"8_CR23","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/B:FORM.0000017721.39909.4b","volume":"24","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Ro\u015fu, G.: An overview of the runtime verification tool Java PathExplorer. Formal Methods Syst. Des. 24(2), 189\u2013215 (2004)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"8_CR24","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"M Kim","year":"2004","unstructured":"Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance approach for Java programs. Form. Methods Syst. Des. 24(2), 129\u2013155 (2004)","journal-title":"Form. Methods Syst. Des."},{"issue":"4","key":"8_CR25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1082983.1083249","volume":"30","author":"M d\u2019Amorim","year":"2005","unstructured":"d\u2019Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. SIGSOFT Softw. Eng. Notes 30(4), 1\u20137 (2005)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44\u201357. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24622-0_5"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-03240-0_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"C Colombo","year":"2009","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 135\u2013149. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03240-0_13"},{"issue":"1","key":"8_CR28","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/s10703-012-0182-0","volume":"43","author":"B Bonakdarpour","year":"2013","unstructured":"Bonakdarpour, B., Navabpour, S., Fischmeister, S.: Time-triggered runtime verification. Formal Methods Syst. Des. 43(1), 29\u201360 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-35632-2_21","volume-title":"Runtime Verification","author":"S Navabpour","year":"2013","unstructured":"Navabpour, S., Bonakdarpour, B., Fischmeister, S.: Path-aware time-triggered runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 199\u2013213. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35632-2_21"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Mastrangelo, L., Hauswirth, M.: JNIF: Java native instrumentation framework. In: Proceedings of the International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools, ser. PPPJ 2014, pp. 194\u2013199. ACM, New York (2014)","DOI":"10.1145\/2647508.2647516"},{"key":"8_CR31","unstructured":"de Lemos, R., Garlan, D., Ghezzi, C., Giese, H.: Software engineering for self-adaptive systems: assurances (Dagstuhl Seminar 13511). Dagstuhl Rep. 3(12), 67\u201396 (2014). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2014\/4508"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57288-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T16:28:17Z","timestamp":1568996897000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57288-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319572871","9783319572888"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57288-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}