{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:31:18Z","timestamp":1742913078721,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319478456"},{"type":"electronic","value":"9783319478463"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-47846-3_13","type":"book-chapter","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T02:53:57Z","timestamp":1476413637000},"page":"193-209","source":"Crossref","is-referenced-by-count":5,"title":["Towards the Formal Verification of Data-Intensive Applications Through Metric Temporal Logic"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Marconi","sequence":"first","affiliation":[]},{"given":"Marcello M.","family":"Bersani","sequence":"additional","affiliation":[]},{"given":"Madalina","family":"Erascu","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,15]]},"reference":[{"unstructured":"Apache Storm. http:\/\/storm.apache.org\/","key":"13_CR1"},{"unstructured":"The Zot bounded satisfiability checker. github.com\/fm-polimi\/zot","key":"13_CR2"},{"doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: Proceedings of LICS, pp. 160\u2013170 (1993)","key":"13_CR3","DOI":"10.1109\/LICS.1993.287591"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11603009_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B B\u00e9rard","year":"2005","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time Petri nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211\u2013225. Springer, Heidelberg (2005). doi: 10.1007\/11603009_17"},{"unstructured":"Bersani, M., Erascu, M., Marconi, F., Rossi, M.: DICE verification tool - initial version. Technical report, DICE Consortium (2016). www.dice-h2020.eu","key":"13_CR5"},{"issue":"4","key":"13_CR6","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1016\/j.jal.2014.07.005","volume":"12","author":"MM Bersani","year":"2014","unstructured":"Bersani, M.M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., Pietro, P.S.: Constraint LTL satisfiability checking without automata. J. Appl. Log. 12(4), 522\u2013557 (2014)","journal-title":"J. Appl. Log."},{"issue":"2","key":"13_CR7","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/s00236-015-0229-y","volume":"53","author":"MM Bersani","year":"2016","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: A tool for deciding the satisfiability of continuous-time metric temporal logic. Acta Informatica 53(2), 171\u2013206 (2016)","journal-title":"Acta Informatica"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-49116-3_30","volume-title":"STACS 99","author":"A Bouajjani","year":"1999","unstructured":"Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 323\u2013333. Springer, Heidelberg (1999). doi: 10.1007\/3-540-49116-3_30"},{"doi-asserted-by":"crossref","unstructured":"Casale, G., Ardagna, D., Artac, M., Barbier, F., Nitto, E.D., Henry, A., Iuhasz, G., Joubert, C., Merseguer, J., Munteanu, V.I., Perez, J., Petcu, D., Rossi, M., Sheridan, C., Spais, I., Vladu\u0161i\u010d, D.: DICE: quality-driven development of data-intensive cloud applications. In: Proceedings of MiSE, pp. 78\u201383 (2015)","key":"13_CR9","DOI":"10.1109\/MiSE.2015.21"},{"issue":"3","key":"13_CR10","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380\u2013415 (2007)","journal-title":"Inf. Comput."},{"doi-asserted-by":"crossref","unstructured":"Demri, S., Gascon, R.: The effects of bounding syntactic resources on Presburger LTL. Technical report LSV-06-5, LSV (2006)","key":"13_CR11","DOI":"10.1109\/TIME.2007.63"},{"issue":"3","key":"13_CR12","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/BF02277857","volume":"7","author":"A Finkel","year":"1994","unstructured":"Finkel, A.: Decidability of the termination problem for completely specified protocols. Distrib. Comput. 7(3), 129\u2013135 (1994)","journal-title":"Distrib. Comput."},{"key":"13_CR13","series-title":"Monographs in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-32332-4","volume-title":"Modeling Time in Computing","author":"CA Furia","year":"2012","unstructured":"Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.: Modeling Time in Computing. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2012)"},{"issue":"2","key":"13_CR14","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"RM Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"13_CR15","volume-title":"The Mathematics of Petri Nets","author":"C Reutenauer","year":"1990","unstructured":"Reutenauer, C.: The Mathematics of Petri Nets. Masson and Prentice, Paris (1990)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47846-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T11:53:36Z","timestamp":1568462016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47846-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319478456","9783319478463"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47846-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}