{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:45:06Z","timestamp":1743137106482,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540401179"},{"type":"electronic","value":"9783540448297"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44829-2_2","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:01:40Z","timestamp":1183478500000},"page":"18-33","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Requirements Patterns-Driven Approach to Specify Systems and Check Properties"],"prefix":"10.1007","author":[{"given":"Sascha","family":"Konrad","sequence":"first","affiliation":[]},{"given":"Laura A.","family":"Campbell","sequence":"additional","affiliation":[]},{"given":"Betty H. C.","family":"Cheng","sequence":"additional","affiliation":[]},{"given":"Min","family":"Deng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"issue":"1","key":"2_CR1","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1023\/A:1008697817793","volume":"6","author":"R. Bharadwaj","year":"1999","unstructured":"Ramesh Bharadwaj and Constance L. Heitmeyer. Model checking complete requirements specifications using abstraction. Automated Software Engineering: An International Journal, 6(1):37\u201368, January 1999.","journal-title":"Automated Software Engineering: An International Journal"},{"key":"2_CR2","unstructured":"Grady Booch, James Rumbaugh, and Ivar Jacobson. The Unified Modeling Language User Guide. Addision-Wesley, 1999."},{"issue":"4","key":"2_CR3","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/s007660200020","volume":"7","author":"L. A. Campbell","year":"2002","unstructured":"Laura A. Campbell, Betty H. C. Cheng, William E. McUmber, and R. E. K. Stirewalt. Automatically detecting and visualizing errors in UML diagrams. Requirements Engineering Journal, 7(4):264\u2013287, 2002.","journal-title":"Requirements Engineering Journal"},{"key":"2_CR4","series-title":"Technical Report","volume-title":"Enabling validation of UML formalizations","author":"B. H. C. Cheng","year":"2002","unstructured":"Betty H. C. Cheng, Laura A. Campbell, Min Deng, and R. E. K. Stirewalt. Enabling validation of UML formalizations. Technical Report MSU-CSE-02-25, Department of Computer Science, Mich State Univ, E Lansing, MI, September 2002."},{"key":"2_CR5","unstructured":"Bruce Powell Douglass. Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison-Wesley, 1999."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In Proceedings 2nd Workshop on Formal Methods in Software Engineering, pages 7\u201316, Clearwater Beach, FL, March 1998.","DOI":"10.1145\/298595.298598"},{"key":"2_CR7","unstructured":"Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994."},{"key":"2_CR8","unstructured":"Wai Ming Ho, Jean-Marc Jezequel, Alain Le Guennec, and Francois Pennaneac\u2019h. UMLAUT: an extendible UML transformation framework. In Proc. of IEEE International Conference on Automated Software Engineering, Cocoa Beach, FL, October 1999."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Gerald J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5), May 1997.","DOI":"10.1109\/32.588521"},{"key":"2_CR10","unstructured":"Honeywell. URL: http:\/\/www.htc.honeywell.com\/dome."},{"key":"2_CR11","unstructured":"I-logix. Rhapsody. URL: http:\/\/www.ilogix.com."},{"key":"2_CR12","unstructured":"Sascha Konrad, Laura A. Campbell, and Betty H. C. Cheng. Adding formal specifications to requirements patterns. In Proceedings of the Requirements for High Assurance Systems Workshop (RHAS02) as part of the IEEE Joint International Conference on Requirements Engineering (RE02), Essen, Germany, September 2002."},{"key":"2_CR13","series-title":"Technical Report","volume-title":"A requirements pattern-driven approach to specify systems and check properties","author":"S. Konrad","year":"2002","unstructured":"Sascha Konrad, Laura A. Campbell, Betty H. C. Cheng, and Min Deng. A requirements pattern-driven approach to specify systems and check properties. Technical Report MSU-CSE-02-28, Computer Science and Engineering, Mich State Univ, E Lansing, MI, December 2002."},{"key":"2_CR14","unstructured":"Sascha Konrad and Betty H. C. Cheng. Requirements patterns for embedded systems. In Proceedings of the IEEE Joint International Conference on Requirements Engineering (RE02), Essen, Germany, September 2002."},{"key":"2_CR15","unstructured":"William E. McUmber and Betty H. C. Cheng. A general framework for formalizing UML with formal languages. In Proceedings of IEEE International Conference on Software Engineering (ICSE01), Toronto, Canada, May 2001."},{"key":"2_CR16","unstructured":"William E. McUmber and Betty H. C. Cheng. UML-based analysis of embedded systems using a mapping to VHDL. In Proceedings of IEEE High Assurance Software Engineering (HASE99), Washington, DC, November 1999."},{"key":"2_CR17","unstructured":"William Eugene McUmber. A Generic Framework for Formalizing Object-Oriented Modeling Notations for Embedded Systems Development. PhD thesis, Michigan State University, August 2000."},{"key":"2_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-45104-8_13","volume-title":"Applications of Graph Transformations with Industrial Relevance AGTIVE","author":"J. Niere","year":"1999","unstructured":"Jorg Niere and Albert Zundorf. Using FUJABA for the development of production control systems. In Applications of Graph Transformations with Industrial Relevance AGTIVE, pages 181\u2013191. Springer Verlag, 1999. Volume 1779, Lecture Notes in Computer Science."},{"key":"2_CR19","unstructured":"Rational. Rational Rose. URL: http:\/\/www.rational.com."},{"key":"2_CR20","unstructured":"Ian Sommerville. Software Engineering. Addison-Wesley, 1992."},{"key":"2_CR21","unstructured":"Telelogic. ObjectGEODE. URL: http:\/\/www.telelogic.com."},{"key":"2_CR22","unstructured":"Anthony Torre. Project specifications for diesel filter system, 2000. http:\/\/www.cse.msu.edu\/~cse470\/F2000\/cheng\/Projects\/F00-Cheng\/filter\/Description\/air-filter.html."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44829-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,6]],"date-time":"2023-02-06T20:15:57Z","timestamp":1675714557000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44829-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540401179","9783540448297"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44829-2_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"15 April 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}