{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:56:50Z","timestamp":1725742610409},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642402289"},{"type":"electronic","value":"9783642402296"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40229-6_8","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:47:40Z","timestamp":1374544060000},"page":"106-120","source":"Crossref","is-referenced-by-count":9,"title":["A Mechanized Semantic Framework for Real-Time Systems"],"prefix":"10.1007","author":[{"given":"Manuel","family":"Garnacho","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mamoun","family":"Filali-Amine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abid, N., Zilio, S.D., Botlan, D.L.: A Verified Approach for Checking Real-Time Specification Patterns. In: Proceedings of VeCos (2012)","DOI":"10.1007\/978-3-642-32469-7_1"},{"key":"8_CR2","unstructured":"Arnold, A.: Finite Transition Systems - Semantics of Communicating Systems. Prentice Hall international series in computer science. Prentice Hall (1994)"},{"key":"8_CR3","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Components in BIP. In: SEFM, pp. 3\u201312 (2006)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/11562948_23","volume-title":"Automated Technology for Verification and Analysis","author":"B. B\u00e9rard","year":"2005","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of Different Semantics for Time Petri Nets. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 293\u2013307. Springer, Heidelberg (2005)"},{"key":"8_CR5","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.\u00a03829, pp. 211\u2013225. Springer, Heidelberg (2005)"},{"key":"8_CR6","unstructured":"Berthomieu, B., Bodeveix, J.-P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F.: Fiacre: an Intermediate Language for Model Verification in the Topcased Environment. In: ERTS 2008 (2008)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development (Coq\u2019Art: The Calculus of Inductive Constructions). Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"8_CR8","unstructured":"Bodeveix, J.-P., Filali, M., Garnacho, M., Spadotti, R., Yang, Z.: On the Mechanization of an AADL Subset. Science of Computer Programming: special issue on Architecture Design Language (submitted, 2013)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/Event-Based Software Model Checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 128\u2013147. Springer, Heidelberg (2004)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. In: STOC, pp. 169\u2013180 (1982)","DOI":"10.1145\/800070.802190"},{"key":"8_CR11","unstructured":"The FIACRE Specification Language for Real-Time Concurrent Systems, http:\/\/projects.laas.fr\/fiacre\/"},{"key":"8_CR12","unstructured":"Garnacho, M., Bodeveix, J.-P., Filali, M.: Mechanized Semantics of Concurrent Systems with Priorities. IRIT Research Report\u20132013-16\u2013FR (2013), http:\/\/www.irit.fr\/~Manuel.Garnacho\/Publications\/MechPrio.pdf"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-642-14052-5_19","volume-title":"Interactive Theorem Proving","author":"H. Geuvers","year":"2010","unstructured":"Geuvers, H., Koprowski, A., Synek, D., van der Weegen, E.: Automated Machine-Checked Hybrid System Safety Proofs. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 259\u2013274. Springer, Heidelberg (2010)"},{"issue":"1\/2","key":"8_CR14","first-page":"151","volume":"3","author":"R. Hale","year":"1993","unstructured":"Hale, R., Cardell-Oliver, R., Herbert, J.: An Embedding of Timed Transition Systems in HOL. FMSD\u00a03(1\/2), 151\u2013174 (1993)","journal-title":"FMSD"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: Temporal Proof Methodologies for Real-time Systems. In: POPL, pp. 353\u2013366 (1991)","DOI":"10.1145\/99583.99629"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/BFb0031995","volume-title":"Real-Time: Theory in Practice","author":"T.A. Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: Timed Transition Systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol.\u00a0600, pp. 226\u2013251. Springer, Heidelberg (1992)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"8_CR18","unstructured":"The ISABELLE System, http:\/\/isabelle.in.tum.de\/"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42\u201354. ACM Press (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-45500-0_15","volume-title":"Theoretical Aspects of Computer Software","author":"C. Paulin-Mohring","year":"2001","unstructured":"Paulin-Mohring, C.: Modelisation of Timed Automata in Coq. In: Kobayashi, N., Babu, C. S. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 298\u2013315. Springer, Heidelberg (2001)"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/3-540-62034-6_36","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"J. Rushby","year":"1996","unstructured":"Rushby, J.: Mechanized Formal Methods: Progress and Prospects. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol.\u00a01180, pp. 43\u201351. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40229-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,1]],"date-time":"2022-03-01T23:09:16Z","timestamp":1646176156000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40229-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642402289","9783642402296"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40229-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}