{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:45:27Z","timestamp":1716770727417},"reference-count":24,"publisher":"Elsevier BV","issue":"8","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Systems and Software"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1016\/j.jss.2012.02.041","type":"journal-article","created":{"date-parts":[[2012,3,8]],"date-time":"2012-03-08T04:49:44Z","timestamp":1331182184000},"page":"1915-1929","source":"Crossref","is-referenced-by-count":18,"title":["Validated templates for specification of complex LTL formulas"],"prefix":"10.1016","volume":"85","author":[{"given":"Salamah","family":"Salamah","sequence":"first","affiliation":[]},{"given":"Ann","family":"Gates","sequence":"additional","affiliation":[]},{"given":"Vladik","family":"Kreinovich","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jss.2012.02.041_bib0005","series-title":"International Conference on Computer Aided Verification CAV","article-title":"NUSMV: a new symbolic model verifier","author":"Cimatti","year":"1999"},{"key":"10.1016\/j.jss.2012.02.041_bib0010","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/j.jss.2012.02.041_bib0015","series-title":"Proceedings of the 21st International Conference on Software Engineering","first-page":"411","article-title":"Patterns in property specification for finite state verification","author":"Dwyer","year":"1999"},{"key":"10.1016\/j.jss.2012.02.041_bib0020","series-title":"Foundamentals of Software Engineering","author":"Ghezzi","year":"2003"},{"issue":"September (8)","key":"10.1016\/j.jss.2012.02.041_bib0025","article-title":"Seven myths of formal methods","volume":"11","author":"Hall","year":"1990","journal-title":"IEEE Software"},{"key":"10.1016\/j.jss.2012.02.041_bib0030","series-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann","year":"2004"},{"issue":"April (4)","key":"10.1016\/j.jss.2012.02.041_bib0035","article-title":"Model checking Java programs using Java PathFinder","volume":"2","author":"Havelund","year":"2000","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/j.jss.2012.02.041_bib0040","series-title":"Proceedings of the Software Engineering and Knowledge Engineering Conference","first-page":"273","article-title":"A property specification tool for generating formal specifications: Prospec 2.0","author":"Gallegos","year":"2008"},{"issue":"October","key":"10.1016\/j.jss.2012.02.041_bib0045","first-page":"112","article-title":"Network OAM requirements for the New York City transit network","author":"Lin","year":"2004","journal-title":"IEEE Communications Magazine"},{"key":"10.1016\/j.jss.2012.02.041_bib0050","series-title":"Proceedings of the 21st International Conference on Software Engineering","first-page":"618","article-title":"Designing safe software for medical devices","author":"MacKenzie","year":"1999"},{"issue":"1","key":"10.1016\/j.jss.2012.02.041_bib0055","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","article-title":"Completing the temporal picture","volume":"83","author":"Manna","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.jss.2012.02.041_bib0060","series-title":"Proceedings of Runtime Verification Workshop, ENTCS, 89(2)","article-title":"Prospec: support for elicitation and formal specification of software properties","author":"Mondragon","year":"2004"},{"issue":"February (1)","key":"10.1016\/j.jss.2012.02.041_bib0065","article-title":"Supporting elicitation and specification of software properties through patterns and composite propositions","volume":"14","author":"Mondragon","year":"2004","journal-title":"International Journal of Software Engineering and Knowledge Engineering"},{"key":"10.1016\/j.jss.2012.02.041_bib0070","series-title":"Proceedings of the IEEE 12th International Symposium on High Assurance Systems Engineering","article-title":"Automated testing of LTL formula generation by Prospec","author":"Munoz","year":"2010"},{"key":"10.1016\/j.jss.2012.02.041_bib0075","unstructured":"National Institute of Standards and Technology (NIST), 2002, June. http:\/\/www.nist.gov\/public-affairs\/releases\/n02-10.htm."},{"issue":"June","key":"10.1016\/j.jss.2012.02.041_bib0080","article-title":"Theorem proving for verification","author":"Rushby","year":"2000","journal-title":"Modelling and Verification of Parallel Processes"},{"key":"10.1016\/j.jss.2012.02.041_bib0085","doi-asserted-by":"crossref","unstructured":"Salamah, S., Gates, A., Roach, S., Engsko, M., 2011. Towards support for software model checking: improving the efficiency of formal specifications. Journal of Advances in Software Engineering, 2011, Article ID 869182.","DOI":"10.1155\/2011\/869182"},{"key":"10.1016\/j.jss.2012.02.041_bib0090","series-title":"12th International SPIN Workshop","article-title":"Verifying pattern-generated LTL formulas: a case study","author":"Salamah","year":"2005"},{"key":"10.1016\/j.jss.2012.02.041_bib0100","unstructured":"Salamah, S., 2007, May. Supporting documentation for dissertation work. The University of Texas at El Paso."},{"key":"10.1016\/j.jss.2012.02.041_bib0105","series-title":"Proceedings of the 21st IEEE-CS International Conference on Software Engineering Education and Training (CSEET)","first-page":"181","article-title":"A technique for using model checkers to teach formal specifications","author":"Salamah","year":"2008"},{"key":"10.1016\/j.jss.2012.02.041_bib0110","series-title":"Proceedings of the 39th Annual Frontiers in Education (FIE) Conference","article-title":"A comparative study of a tool-based approach to teaching formal specifications","author":"Salamah","year":"2010"},{"key":"10.1016\/j.jss.2012.02.041_bib0115","series-title":"Proceedings of the Fifth Workshop on Runtime Verification","article-title":"Temporal assertions using AspectJ","author":"Stolz","year":"2005"},{"key":"10.1016\/j.jss.2012.02.041_bib0120","unstructured":"The Economic Impacts of Inadequate Infrastructure for Software Testing, 2002. Health, Social, and Economic Research, Project No. 7007,001. Resaerch Triangle Park, NC."},{"key":"10.1016\/j.jss.2012.02.041_bib0125","unstructured":"Vela, C.Y., 2009. An implementation for automatic generation of linear temporal logic formulas. Master's Project. Department of Computer Science, The University of Texas at El Paso."}],"container-title":["Journal of Systems and Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121212000659?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121212000659?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,6,24]],"date-time":"2019-06-24T22:34:48Z","timestamp":1561415688000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0164121212000659"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":24,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["S0164121212000659"],"URL":"https:\/\/doi.org\/10.1016\/j.jss.2012.02.041","relation":{},"ISSN":["0164-1212"],"issn-type":[{"value":"0164-1212","type":"print"}],"subject":[],"published":{"date-parts":[[2012,8]]}}}
