{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:49:37Z","timestamp":1760586577021,"version":"3.37.3"},"reference-count":7,"publisher":"Wiley","license":[{"start":{"date-parts":[[2011,6,22]],"date-time":"2011-06-22T00:00:00Z","timestamp":1308700800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["HRD 0734825"],"award-info":[{"award-number":["HRD 0734825"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Advances in Software Engineering"],"published-print":{"date-parts":[[2011,6,22]]},"abstract":"<jats:p>The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et al., to generate formal specifications in Linear Temporal Logic (LTL) and other languages. The work\npresented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the B\u00fcchi automaton generated for the formula. Minimizing the size of the B\u00fcchi automata for an LTL specification provides a significant improvement for model checking software systems using such tools as the highly acclaimed Spin model checker.<\/jats:p>","DOI":"10.1155\/2011\/869182","type":"journal-article","created":{"date-parts":[[2011,6,22]],"date-time":"2011-06-22T19:01:09Z","timestamp":1308769269000},"page":"1-13","source":"Crossref","is-referenced-by-count":4,"title":["Towards Support for Software Model Checking: Improving the Efficiency of Formal Specifications"],"prefix":"10.1155","volume":"2011","author":[{"given":"Salamah","family":"Salamah","sequence":"first","affiliation":[{"name":"Department of Electrical, Computer, Software, and Systems Engineering, Embry-Riddle Aeronautical University (ERAU), Daytona Beach, FL 32114, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ann Q.","family":"Gates","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Texas at El Paso (UTEP), El Paso, TX 79968, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Roach","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Texas at El Paso (UTEP), El Paso, TX 79968, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Engskow","sequence":"additional","affiliation":[{"name":"Department of Electrical, Computer, Software, and Systems Engineering, Embry-Riddle Aeronautical University (ERAU), Daytona Beach, FL 32114, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","reference":[{"key":"10","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2817"},{"year":"1999","key":"1"},{"year":"2004","key":"8"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194004001567"},{"issue":"1","key":"12","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","year":"1991","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"9","first-page":"366","volume":"2","year":"2000","journal-title":"In-\nternational Journal on Software Tools for Technology Transfer"},{"year":"1995","key":"7"}],"container-title":["Advances in Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/archive\/2011\/869182.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/archive\/2011\/869182.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/archive\/2011\/869182.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T00:50:57Z","timestamp":1607475057000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.hindawi.com\/journals\/ase\/2011\/869182\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6,22]]},"references-count":7,"alternative-id":["869182","869182"],"URL":"https:\/\/doi.org\/10.1155\/2011\/869182","relation":{},"ISSN":["1687-8655","1687-8663"],"issn-type":[{"type":"print","value":"1687-8655"},{"type":"electronic","value":"1687-8663"}],"subject":[],"published":{"date-parts":[[2011,6,22]]}}}