{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T02:45:08Z","timestamp":1783478708082,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540281955","type":"print"},{"value":"9783540318996","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11537328_17","type":"book-chapter","created":{"date-parts":[[2010,7,22]],"date-time":"2010-07-22T20:02:25Z","timestamp":1279828945000},"page":"200-220","source":"Crossref","is-referenced-by-count":5,"title":["Verifying Pattern-Generated LTL Formulas: A Case Study"],"prefix":"10.1007","author":[{"given":"Salamah","family":"Salamah","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ann","family":"Gates","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Roach","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Oscar","family":"Mondragon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/192218.192226","volume":"3","author":"L. Dillon","year":"1994","unstructured":"Dillon, L., Kutty, G., Moser, L.E., Melliar \u2013Smith, P.M., Ramakrishna, Y.S.: A Graphical Interval Logic for Specifying Concurrent Systems. ACM Transactions on Software Eng. and Methodology\u00a03, 131\u2013165 (1994)","journal-title":"ACM Transactions on Software Eng. and Methodology"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property Specification Patterns for Finite\u2013State Verification. In: Proceedings of the 2nd Workshop on Formal Methods in Software Practice, Clearwater Beach, Florida, pp. 7\u201315 (1998)","DOI":"10.1145\/298595.298598"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specification for Finite\u2013State Verification. In: Proceedings of the 21st Intl. Conference on Software Engineering, Los Angeles, CA, USA, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"17_CR4","first-page":"416","volume-title":"Design Patterns, Elements of Reusable Object\u2013 Oriented Software","author":"E. Gamma","year":"1995","unstructured":"Gamma, E., Helm, R.: Design Patterns, Elements of Reusable Object\u2013 Oriented Software, p. 416. Addison Wesley, Reading (1995)"},{"key":"17_CR5","unstructured":"Kutty, G.: A Graphical Environment for Temporal Reasoning. Dissertation, Electrical and Computer Engineering Department, University of California at Santa Barbara (1994)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Schnoebelen, P.: Specification in CTL+Past for Verification in CTL. Information and Computation, 236\u2013263 (2000)","DOI":"10.1006\/inco.1999.2817"},{"issue":"1","key":"17_CR7","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the Temporal Picture. Theoretical Computer Science\u00a083(1), 97\u2013130 (1991)","journal-title":"Theoretical Computer Science"},{"key":"17_CR8","unstructured":"Merriam Webster Online (April 2005), http:\/\/www.m-w.com\/cgi-bin\/dictionary?book=Dictionary&va=follow"},{"key":"17_CR9","unstructured":"Mondragon, O., Gates, A., Roach, S.: Composite Propositions: Toward Support for Formal Specification of System Properties. In: Proceedings of the 27th Annual IEEE\/NASA Goddard Software Engineering Workshop, Greenbelt, MD, USA (December 2002)"},{"key":"17_CR10","unstructured":"Mondragon, O., Gates, A.Q., Roach, S.: Prospec: Support for Elicitation and Formal Specification of Software Properties. In: Sokolsky, O., Viswanathan, M. (eds.) Proceedings of Runtime Verification Workshop. ENTCS, vol.\u00a089(2) (2004)"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Mondragon, O., Gates, A.Q.: Supporting Elicitation and Specification of Software Properties through Patterns and Composite Propositions. Intl. Journal Software Engineering and Knowledge Engineering\u00a0XS 14(1) (February 2004)","DOI":"10.1142\/S0218194004001567"},{"key":"17_CR12","unstructured":"Mondragon, O.: Elucidation and Specification of Software Properties through Patterns and Composite Propositions to Support Formal Verification Techniques. Dissertation, The University of Texas at El Paso (May 2004)"},{"key":"17_CR13","unstructured":"Salamah, S.: Supporting Documentation for the SPS-Prospec Case Study, UTEP-CS-05-14, the University of Texas at El Paso (April 2005)"},{"key":"17_CR14","unstructured":"Spec Patterns (April 2005), http:\/\/patterns.projects.cis.ksu.edu\/"},{"key":"17_CR15","unstructured":"Spec Patterns (April 2005), http:\/\/patterns.projects.cis.ksu.edu\/documentation\/patterns\/scopes.shtml"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11537328_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:12:32Z","timestamp":1605643952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11537328_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540281955","9783540318996"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11537328_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}