{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:07:49Z","timestamp":1773655669542,"version":"3.50.1"},"reference-count":23,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,10,1]],"date-time":"2003-10-01T00:00:00Z","timestamp":1064966400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2003,10,1]],"date-time":"2003-10-01T00:00:00Z","timestamp":1064966400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3589,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,10]]},"DOI":"10.1016\/s1571-0661(04)81043-0","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"67-88","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":14,"title":["Prospec"],"prefix":"10.1016","volume":"89","author":[{"given":"Oscar","family":"Mondrag\u00f3n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ann Q.","family":"Gates","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"Roach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB1","doi-asserted-by":"crossref","unstructured":"Chang S., Z. Manna, and A. Pnueli, \u201cCharacterization of Temporal Property Classes,\u201d in W. Kuich (eds.): Proceedings of the 19th Intl. Colloquium on Automata, Languages, and Programming, LNCS 623, Springer\u2013Verlag, 1992, 474\u2013486.","DOI":"10.1007\/3-540-55719-9_97"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB2","unstructured":"Delgado N., \u201cA Taxonomy of Dynamic Software-Fault Monitoring Tools,\u201d Master Thesis, The University of Texas at El Paso, 2001."},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB3","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1145\/192218.192226","article-title":"A Graphical Interval Logic for Specifying Concurrent Systems","volume":"3","author":"Dillon","year":"1994","journal-title":"ACM Transactions on Software Eng. and Methodology"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB4","doi-asserted-by":"crossref","unstructured":"Dulac N., T. Viguier, N. Leveson, and M. A. Storey, \u201cOn the Use of Visualization in Formal Requirements Specification\u201d, Proceedings of the IEEE Joint Int. Conference on Requirements Engineering (RE '02), Essen, Germany, August 2002, 71\u201380.","DOI":"10.1109\/ICRE.2002.1048507"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB5","doi-asserted-by":"crossref","unstructured":"Dwyer, M. B., G. S. Avrunin, and J. C. Corbett, \u201cProperty Specification Patterns for Finite\u2013State Verification,\u201d 2nd Workshop on Formal Methods in Software Practice. Clearwater Beach, Florida, 1998, 7\u201315.","DOI":"10.1145\/298595.298598"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Dwyer, M. B., G. S. Avrunin, and J. C. Corbett, \u201cPatterns in Property Specification for Finite\u2013State Verification,\u201d 21st Intl. Conference on Software Engineering, Los Angeles, CA, USA, 1999, 411\u2013420.","DOI":"10.1145\/302405.302672"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB7","series-title":"\u201cDesign Patterns, Elements of Reusable Object\u2013Oriented Software,\u201d","first-page":"416","author":"Gamma","year":"1995"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB8","series-title":"\u201cAn Introduction to Discrete Mathematics and Formal System Specifications,\u201d","author":"Ince","year":"1988"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB9","unstructured":"Kim M., M. Viswanathan, et al., \u201cFormally Specified Monitoring of Temporal Properties,\u201d in Proceedings of the 11th Euromicro Conference on Real\u2013Time Systems, York, UK, June 1999, 114\u2013121."},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB10","unstructured":"Kutty G., \u201cA Graphical Environment for Temporal Reasoning,\u201d Dissertation, Electrical and Computer Engineering Department, University of California at Santa Barbara, 1994."},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB11","unstructured":"Kim M., S. Kannan, et al., \u201cJava-Mac: a Run-time Assurance Tool for Java Programs,\u201d in Proceedings of Runtime Verification 2001, ENTCS, 55 (2001)."},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB12","unstructured":"Kim M., M. Viswanathan, et al., \u201cMaC: A Framework for Run\u2013time Correctness Assurance of Real\u2013Time Systems,\u201d Technical Report, 1998."},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB13","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the Correctness of Multiprocess Programs","volume":"3","author":"Lamport","year":"1977","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB14","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1006\/inco.1999.2817","article-title":"Specification in CTL+Past for Verification in CTL","author":"Laroussinie","year":"2000","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB15","doi-asserted-by":"crossref","unstructured":"Lecoeuche R., C. Mellish, and D. Robertson, \u201cA Framework for Requirements Elicitation through Mixed\u2013Initiative Dialogue,\u201d Third IEEE Intl. Conference on Requirements Engineering, Colorado Springs, USA, April 1998, 190\u2013196.","DOI":"10.1109\/ICRE.1998.667825"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB16","series-title":"Program Design Calculi, NATO ASI 118, Series F: Computer and System Sciences","first-page":"287","article-title":"\u201cA Temporal Proof Methodology for Reactive Systems,\u201d","author":"Manna","year":"1993"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB17","unstructured":"Mondragon O., A. Gates, and S. Roach, \u201cComposite Propositions: Toward Support for Formal Specification of System Properties,\u201d Proceedings of the 27th Annual IEEE\/NASA Goddard Software Engineering Workshop, Greenbelt, MD, USA, December 2002."},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB18","first-page":"730","article-title":"The Programming Language Tempura","volume":"22","author":"Moszkowski","year":"1996","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB19","doi-asserted-by":"crossref","unstructured":"Ramakrishna Y., P. Melliar-Smith, et al., \u201cReally Visual Temporal Reasoning,\u201d in Proceedings of 14th Real\u2013Time Systems Symposium, Raleigh\u2013Durham, NC, 1993, 262\u2013273.","DOI":"10.1109\/REAL.1993.393490"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB20","doi-asserted-by":"crossref","unstructured":"Schwartz R., P. Melliar-Smith, et al., \u201cAn Interval Logic for Higher-Level Temporal Reasoning,\u201d in Proceedings of the Second Annual ACM SIGACT\u2013SIGOPS Symposium on Principles of Distributed Computing, Montreal, August 1983, 173\u2013186.","DOI":"10.1145\/800221.806720"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB21","doi-asserted-by":"crossref","unstructured":"Smith R., G. Avrunin, L. Clarke, and L. Osterweil, \u201cPROPEL: An Approach Supporting Property Elucidation, in Proceedings Intl. Conference on Software Engineering, Orlando, FL, USA, May 2002, 11\u201321.","DOI":"10.1109\/ICSE.2002.1007952"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB22","doi-asserted-by":"crossref","unstructured":"Smith, M. H., G. J. Holzmann, and K. Etessami, \u201cEvents and Constraints: a Graphical Editor for Capturing Logic Requirements of Programs,\u201d Sixth IEEE Intl. Symposium on Requirements Engineering, Toronto, Canada, August 2001, 14\u201322.","DOI":"10.1109\/ISRE.2001.948539"},{"key":"10.1016\/S1571-0661(04)81043-0_NEWBIB23","series-title":"High Integrity Software","first-page":"115","article-title":"Bay Area Rapid Transit District Advance Automated Train Control System Case Study Description","author":"Winter","year":"2001"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104810430?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104810430?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:06:27Z","timestamp":1761609987000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104810430"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,10]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,10]]}},"alternative-id":["S1571066104810430"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)81043-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,10]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Prospec","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)81043-0","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2003 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}