{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T03:50:14Z","timestamp":1648871414332},"reference-count":30,"publisher":"Elsevier","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1016\/s0065-2458(08)60643-9","type":"book-chapter","created":{"date-parts":[[2008,5,30]],"date-time":"2008-05-30T08:21:49Z","timestamp":1212135709000},"page":"141-178","source":"Crossref","is-referenced-by-count":1,"title":["Using Model Checking to Analyze Requirements and Designs"],"prefix":"10.1016","author":[{"given":"Joanne","family":"Atlee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Gannon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0065-2458(08)60643-9_bib1","doi-asserted-by":"crossref","unstructured":"Allen, R. & Garlan, D. (1994). Formalizing architectural connection. Proc. Sixteenth International Conference on Software Engineering, May 1994","DOI":"10.1109\/ICSE.1994.296767"},{"key":"10.1016\/S0065-2458(08)60643-9_bib2","unstructured":"Alspaugh, T., Faulk, S., Britton, K., Parker, R., Parnas, D. & Shore, J. (1988). Software Requirements for the A-7E Aircraft. Technical Report, Naval Research Laboratory"},{"key":"10.1016\/S0065-2458(08)60643-9_bib3","unstructured":"Atlee, J. (1992). \u201cAutomated analysis of software requirements.\u201d Ph.D. Thesis, University of Maryland, College Park, MD"},{"issue":"7","key":"10.1016\/S0065-2458(08)60643-9_bib4","first-page":"22","article-title":"State-based model checking of event-driven system requirements","volume":"19","author":"Atlee","year":"1993","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0065-2458(08)60643-9_bib5","doi-asserted-by":"crossref","unstructured":"Atlee, Joanne, M., and Buckley, Michael, A. (1996). A logic-model semantics for SCR software requirements. Proc. 1996 International Symposium on Software Testing and Analysis (ISSTA), pp. 280\u2013292, January 1996","DOI":"10.1145\/229000.226326"},{"key":"10.1016\/S0065-2458(08)60643-9_bib6","doi-asserted-by":"crossref","unstructured":"Atlee, Joanne, M., and Gannon, John (1993). Analyzing timing requirements. Proc. 1993 International Symp. on Software Testing and Analysis (ISSTA), pp. 117\u2013127, Cambridge, MA, June 1993","DOI":"10.1145\/154183.154264"},{"issue":"2","key":"10.1016\/S0065-2458(08)60643-9_bib7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1109\/32.345823","article-title":"Model checking in practice: The t9000 virtual channel processor","volume":"21","author":"Barrett","year":"1995","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0065-2458(08)60643-9_bib8","unstructured":"Browne, M. (1989). \u201cAutomatic verification of finite state machines using temporal logic.\u201d Ph.D. Thesis, Carnegie Mellon University, 1989"},{"key":"10.1016\/S0065-2458(08)60643-9_bib9","doi-asserted-by":"crossref","unstructured":"Bultan, Tevfik, Fischer, Jeffrey, and Gerber, Richard (1996). Compositional verification by model checking for counter-examples. Proc. 1996 International Symp. on Software Testing and Analysis (ISSTA), pp. 224\u2013238, January 1996","DOI":"10.1145\/229000.226321"},{"key":"10.1016\/S0065-2458(08)60643-9_bib10","doi-asserted-by":"crossref","unstructured":"Chechik, M. & Gannon, J. (1994). Automatic verification of requirements implementations. Proc. 1994 International Symp. on Software Testing and Analysis (ISSTA), pp. 1\u201314, Seattle, WA, August 1994","DOI":"10.1145\/186258.186324"},{"key":"10.1016\/S0065-2458(08)60643-9_bib11","doi-asserted-by":"crossref","unstructured":"Chechik, M. & Gannon, J. (1995). Automatic analysis of consistency between implementations and requirements: A case study. Proc. 10th Annual Conference on Computer Assurance, pp. 123\u2013131, June 1995","DOI":"10.1109\/CMPASS.1995.521892"},{"key":"10.1016\/S0065-2458(08)60643-9_bib12","unstructured":"Chechik, M. & Gannon, J. (1995). Automatic analysis of consistency between requirements and designs. Technical Report CS-TR-3394.1, Dept. of Computer Science, University of Maryland, College Park"},{"key":"10.1016\/S0065-2458(08)60643-9_bib13","doi-asserted-by":"crossref","unstructured":"Clarke, Edmund, M., Grumberg, Orna, and Long, David, E. (1992). Model checking and abstraction. Proc. Ninth Annual Symp. on Principles of Programming Languages, pp. 343\u2013354, August 1992","DOI":"10.1145\/143165.143235"},{"key":"10.1016\/S0065-2458(08)60643-9_bib14","volume":"131","author":"Clarke","year":"1981"},{"issue":"2","key":"10.1016\/S0065-2458(08)60643-9_bib15","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Trans. Programming Languages Syst."},{"key":"10.1016\/S0065-2458(08)60643-9_bib16","unstructured":"Cousot, Patrick, and Cousot, Radhia (1976). Static determination of dynamic properties of programs. Proc. Colloque sur la Programmation, April 1976"},{"key":"10.1016\/S0065-2458(08)60643-9_bib17","doi-asserted-by":"crossref","unstructured":"Cousot, Patrick, and Cousot, Radhia (1977). Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proc. 4th POPL, pp. 238\u2013252, Los Angeles, CA","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/S0065-2458(08)60643-9_bib18","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"StateCharts: A visual formalism for complex systems","volume":"8","author":"Harel","year":"1987","journal-title":"Sci. Computer Programming"},{"key":"10.1016\/S0065-2458(08)60643-9_bib19","unstructured":"Heitmeyer, C. (1994). Tools for analyzing requirements: A formal foundation, paper presented at the Fourth International SCR Workshop, December 1994"},{"key":"10.1016\/S0065-2458(08)60643-9_bib20","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C. & Labaw, B. (1993). Consistency checks for SCR-style requirements specifications. Technical Report NRL 93\u20139586, Naval Research Laboratory","DOI":"10.21236\/ADA276077"},{"key":"10.1016\/S0065-2458(08)60643-9_bib21","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C., Labaw, B. & Kiskis, D. (1995). Consistency checking of SCR-style requirements specifications. Proc. RE'95 International Symp. of Requirements Engineering, March 1995","DOI":"10.1109\/ISRE.1995.512546"},{"issue":"1","key":"10.1016\/S0065-2458(08)60643-9_bib22","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/TSE.1980.230208","article-title":"Specifying software requirements for complex systems: New techniques and their applications","volume":"SE-6","author":"Heninger","year":"1980","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0065-2458(08)60643-9_bib23","doi-asserted-by":"crossref","unstructured":"Jackson, Daniel, and Damon, Craig, A. (1996). Elements of style: Analyzing a software design feature with a counterexample detector. Proc. 1996 International Symp. on Software Testing and Analysis (ISSTA), pp. 239\u2013249, January 1996","DOI":"10.1145\/229000.226322"},{"issue":"9","key":"10.1016\/S0065-2458(08)60643-9_bib24","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1109\/32.317428","article-title":"Requirements specification for process-control systems","volume":"20","author":"Leveson","year":"1994","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0065-2458(08)60643-9_bib25","series-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"10.1016\/S0065-2458(08)60643-9_bib26","unstructured":"Parnas, D. & Madey, J. (1991). Functional documentation for computer systems engineering (version 2). Technical Report CRL 237, McMaster University, Department of Electrical and Computer Engineering"},{"key":"10.1016\/S0065-2458(08)60643-9_bib27","unstructured":"Parnas, D.L. (1993). Some theorems we should prove. Proc. 1993 International Conference on HOL Therem Proving and Its Applications, Vancouver, BC, August 1993"},{"key":"10.1016\/S0065-2458(08)60643-9_bib28","unstructured":"Sreemani, Tirumale, and Atlee, Joanne, M. (1995). Feasibility of model checking software requirements: A case study. Technical Report CS-95\u201348, Department of Computer Science, University of Waterloo"},{"key":"10.1016\/S0065-2458(08)60643-9_bib29","unstructured":"van Schouwen, A.J. (1990). The A-7 requirements model: Re-examination for real-time systems and an application to monitoring systems. Technical Report TR-90\u2013276, Queen's University, Kingston, Ontario"},{"key":"10.1016\/S0065-2458(08)60643-9_bib30","doi-asserted-by":"crossref","unstructured":"Wing, Jeannette, and Vaziri-Farahani, Mandana (1995). Model checking software systems: A case study. Proc. 3rd Symp. on the Foundations of Software Engineering, pp. 128\u2013139, October 1995","DOI":"10.1145\/222124.222148"}],"container-title":["Advances in Computers"],"original-title":[],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T18:52:12Z","timestamp":1557600732000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0065245808606439"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1016\/s0065-2458(08)60643-9","relation":{},"ISSN":["0065-2458"],"issn-type":[{"value":"0065-2458","type":"print"}],"subject":[],"published":{"date-parts":[[1996]]}}}