{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:19:16Z","timestamp":1759033156307},"reference-count":29,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[1993]]},"DOI":"10.1109\/32.210305","type":"journal-article","created":{"date-parts":[[2002,8,24]],"date-time":"2002-08-24T23:09:11Z","timestamp":1030230551000},"page":"24-40","source":"Crossref","is-referenced-by-count":144,"title":["State-based model checking of event-driven system requirements"],"prefix":"10.1109","volume":"19","author":[{"given":"J.M.","family":"Atlee","sequence":"first","affiliation":[]},{"given":"J.","family":"Gannon","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/32.60312"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"ref12","author":"faulk","year":"1989","journal-title":"State Determination in Hard-Embedded Systems"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/103167.103173"},{"key":"ref14","article-title":"Integrating automata and temporal logic: A framework for specification of real-time systems and software","author":"gabrielian","year":"1990","journal-title":"The Unified Computation Laboratory"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(90)90074-V"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/32.54292"},{"key":"ref18","year":"0"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1980.230208"},{"key":"ref28","author":"van schouwen","year":"1991","journal-title":"private communication"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10009-1_7"},{"key":"ref27","author":"van schouwen","year":"1990","journal-title":"The A-7 Requirements Model Reexamination for Real-Time Systems and an Application to Monitoring Systems"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/125083.123047"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676711"},{"key":"ref29","author":"weiss","year":"1992","journal-title":"private communication"},{"key":"ref5","author":"browne","year":"1989","journal-title":"Automatic Verification of Finite State Machines Using Temporal Logic"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"ref7","first-page":"428","article-title":"Symbolic model checking: 10<superscript>20<\/superscript> states and beyond","author":"burch","year":"1990","journal-title":"Proc 11th Annu Symp Logic in Computer Science"},{"key":"ref2","author":"atlee","year":"1992","journal-title":"Automated Analysis of Software Requirements"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/5.97298"},{"key":"ref1","author":"alspaugh","year":"1988","journal-title":"Software requirements for the A-7E aircraft"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6313045"},{"key":"ref22","doi-asserted-by":"crossref","DOI":"10.21236\/ADA227320","author":"manna","year":"1990","journal-title":"Tools and rules for the practicing verifier"},{"key":"ref21","author":"kirby","year":"1987","journal-title":"Example NRL\/SCR software requirements for an automobile cruise control and monitoring system"},{"key":"ref24","author":"parnas","year":"1988","journal-title":"Making formal software documentation more practical A progress report"},{"key":"ref23","author":"ostroff","year":"1989","journal-title":"Temporal Logic for Real-Time Systems"},{"key":"ref26","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1109\/CMPSAC.1988.17148","article-title":"STATEMATE and cruise control: A case<superscript>2<\/superscript> study","author":"smith","year":"1988","journal-title":"Proc COMPAC'88 12th Int IEEE Computer Software and Application Conf"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx1\/32\/5456\/00210305.pdf?arnumber=210305","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:08:44Z","timestamp":1638216524000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/210305\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":29,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/32.210305","relation":{},"ISSN":["0098-5589"],"issn-type":[{"value":"0098-5589","type":"print"}],"subject":[],"published":{"date-parts":[[1993]]}}}