{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,5]],"date-time":"2024-12-05T05:25:14Z","timestamp":1733376314114,"version":"3.30.1"},"reference-count":41,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4946,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2000,1]]},"DOI":"10.1016\/s0167-6423(99)00018-0","type":"journal-article","created":{"date-parts":[[2002,10,31]],"date-time":"2002-10-31T21:12:04Z","timestamp":1036098724000},"page":"65-96","source":"Crossref","is-referenced-by-count":3,"title":["On the analysis needs when verifying state-based software requirements: an experience report"],"prefix":"10.1016","volume":"36","author":[{"given":"Mats P.E.","family":"Heimdahl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara J.","family":"Czerny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0167-6423(99)00018-0_BIB1","doi-asserted-by":"crossref","unstructured":"R.J. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D. Notkin, J.D. Reese, Model checking large software specifications, in: D. Garlan (Ed.), Proc. 4th ACM SIGSOFT Symp. on the Foundations of Software Engineering (SIGSOFT\u2019 96), October 1996.","DOI":"10.1145\/239098.239127"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB2","doi-asserted-by":"crossref","unstructured":"J.M. Atlee, M.A. Buckley, A logic-model semantics for SCR software requirements, in: S.J. Zeil (Ed.), Proc. ACM SIGSOFT Int. Symp. on Software Testing and Analysis (ISSTA\u2019 96), January 1996, pp. 280\u2013292.","DOI":"10.1145\/229000.226326"},{"issue":"1","key":"10.1016\/S0167-6423(99)00018-0_BIB3","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/32.210305","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\/S0167-6423(99)00018-0_BIB4","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, J. Levitt, Validity checking for combinations of theories with equality, in: M. Srivas, A. Camilleri (Eds.), Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science, vol. 1166, Springer, Berlin, November 1996, pp. 187\u2013201. Palo Alto, CA, November 6\u20138.","DOI":"10.1007\/BFb0031808"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB5","doi-asserted-by":"crossref","unstructured":"S. Bensalam, Y. Lakhnech, H. Saidi, Powerful techniques for the automatic generation of invariants, in: R. Alur, T.A. Henzinger (Eds.), Proc. 8th Int. Conf. on Computer Aided Verification, CAV\u2019 96, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, August 1996, pp. 323\u2013335.","DOI":"10.1007\/3-540-61474-5_80"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB6","unstructured":"R. Bharadwaj, C. Heitmeyer, Verifying SCR requirements specifications using state exploration, in: 1st ACM SIGPLAN Workshop on Automatic Analysis of Software, January 1997."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB7","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, Graph-based algorithms for boolean function manipulation, IEEE Trans. Comput. C-35(8) (1986) 677\u2013691.","DOI":"10.1109\/TC.1986.1676819"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB8","doi-asserted-by":"crossref","unstructured":"M. Chechik, J. Gannon, Automatic verification of requirements implementations, in: Proc. ACM SIGSOFT Int. Symp. on Software Testing and Analysis, 1994, pp. 1\u201314.","DOI":"10.1145\/186258.186324"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB9","doi-asserted-by":"crossref","unstructured":"M. Chechik, J. Gannon, Automatic analysis of consistency between implementations and requirements: a case study, in: Proc. 10th Annual Conf. on Computer Assurance, COMPASS 95, 1995, pp. 123\u2013131.","DOI":"10.1109\/CMPASS.1995.521892"},{"issue":"5","key":"10.1016\/S0167-6423(99)00018-0_BIB10","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM Trans. Programm. Lang. Systems"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB11","unstructured":"J. Crow, S. Owre, J. Rushby et al., A tutorial introduction to PVS, in: WIFT 95: Workshop on Industrial-Strength Formal Specification Techniques, 1995."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB12","unstructured":"B.J. Czerny, Integrative analysis of state-based requirements for completeness and consistency, Ph.D. Thesis, Michigan State University, May 1998."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB13","doi-asserted-by":"crossref","unstructured":"B.J. Czerny, M.P.E. Heimdahl, Automated integrative analysis of state-based requirements, in: Proc. 13th IEEE Int. Conf. on Automated Software Engineering (ASE\u201998), Honolulu, Hawaii, October 1998, pp. 125\u2013134.","DOI":"10.1109\/ASE.1998.732601"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB14","doi-asserted-by":"crossref","unstructured":"D. Harel, Statecharts: a visual formalism for complex systems, Sci. Comput. Programm. (1987) 231\u2013274.","DOI":"10.1016\/0167-6423(87)90035-9"},{"issue":"5","key":"10.1016\/S0167-6423(99)00018-0_BIB15","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1145\/42411.42414","article-title":"On visual formalisms","volume":"31","author":"Harel","year":"1988","journal-title":"Commun. ACM"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB16","doi-asserted-by":"crossref","unstructured":"D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, M. Trakhtenbrot, Statemate: a working environment for the development of complex reactive systems, IEEE Trans. Software Eng. 16(4) (1990) 403\u2013414.","DOI":"10.1109\/32.54292"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB17","doi-asserted-by":"crossref","unstructured":"D. Harel, A. Pnueli, On the development of reactive systems, in: K.R. Apt (Ed.), Logics and Models of Concurrent Systems, Springer, Berlin, 1985, pp. 477\u2013498.","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB18","doi-asserted-by":"crossref","unstructured":"M.P.E. Heimdahl, N.G. Leveson, Completeness and consistency analysis of state-based requirements, IEEE Trans. Software Eng. TSE-22(6) (1996) 363\u2013377.","DOI":"10.1109\/32.508311"},{"issue":"3","key":"10.1016\/S0167-6423(99)00018-0_BIB19","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1145\/234426.234431","article-title":"Automated consistency checking of requirements specifications","volume":"5","author":"Heitmeyer","year":"1996","journal-title":"ACM Trans. Software Eng. Methodol."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB20","doi-asserted-by":"crossref","unstructured":"C.L. Heitmeyer, B.L. Labaw, D. Kiskis, Consistency checking of SCR-style requirements specifications, in: Proc. 2nd IEEE Int. Symp. on Requirements Engineering, March 1995.","DOI":"10.1109\/ISRE.1995.512546"},{"issue":"1","key":"10.1016\/S0167-6423(99)00018-0_BIB21","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 application","volume":"6","author":"Heninger","year":"1980","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB22","unstructured":"G.J. Holzmann, Design and Validation of Computer Protocols, Prentice-Hall, Englewood Cliffs, NJ, 1991."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB23","article-title":"Requirements specification for process-control systems","volume":"1994","author":"Leveson","year":"684706","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB24","unstructured":"N.G. Leveson, M. Heimdahl, H. Hildreth, J. Reese, TCAS II requirements specification."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB25","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Dordrecht, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB26","doi-asserted-by":"crossref","unstructured":"S.P. Miller, M. Srivas, Formal verification of the AAMP5 microprocessor, in: Proc. Int. Workshop on Industrial Strength Formal Techniques, 1995, pp. 2\u201317.","DOI":"10.1109\/WIFT.1995.515475"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB27","unstructured":"S. Owre, N. Shankar, J.M. Rushby, The PVS Specification Language, Computer Science Laboratory; SRI International, Menlo Park, CA 94025, beta release edition, April 1993."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB28","unstructured":"S. Owre, N. Shankar, J.M. Rushby, User Guide for the PVS Specification and Verification System, Computer Science Laboratory; SRI International, Menlo Park, CA 94025, beta release edition, March 1993."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB29","doi-asserted-by":"crossref","unstructured":"D.Y.W. Park, J.U. Skakkeb\u00e6k, D.L. Dill, Static analysis to identify invariants in RSML specifications, in: Formal Techniques in Real-Time and Fault Tolerant Systems, Lyngby, Denmark, September 1998.","DOI":"10.1007\/BFb0055343"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB30","doi-asserted-by":"crossref","unstructured":"D.Y.W. Park, J.U. Skakkeb\u00e6k, M.P.E. Heimdahl, B.J. Czerny, D.L. Dill, Checking properties of safety critical specifications using efficient decision procedures, in: Proc. FMSP\u2019 98: Workshop on Formal Methods in Software Practice, March 1998.","DOI":"10.1145\/298595.298603"},{"issue":"8","key":"10.1016\/S0167-6423(99)00018-0_BIB31","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/135226.135233","article-title":"A practical algorithm for exact array dependence analysis","volume":"35","author":"Pugh","year":"1992","journal-title":"Commun. ACM"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB32","unstructured":"J.M. Rushby, personal communication, 1995."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB33","unstructured":"J. Rushby, Formal specification and verification for critical systems: Tools, achievements, and prospects, in: Electric Power Research Institute (EPRI) Workshop on Methodologies for Cost-Effective, Reliable Software Verification and Validation, January 1992, pp. 9\u20131 to 9\u201314."},{"issue":"1","key":"10.1016\/S0167-6423(99)00018-0_BIB34","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1109\/32.210304","article-title":"Formal verification of algorithms for critical systems","volume":"19","author":"Rushby","year":"1993","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB35","doi-asserted-by":"crossref","unstructured":"R.M. Smullyan, First-Order Logic, Springer, New York, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB36","unstructured":"N. Shankar, Mechanical verification of a schematic protocol for byzantine fault-tolerant clock synchronization, Technical Report SRI-CSL-91-04, SRI International, June 1991."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB37","unstructured":"N. Shankar, S. Owre, J.M. Rushby, The PVS Proof Checker: A Reference Manual, Computer Science Laboratory; SRI International, Menlo Park, CA 94025, beta release edition, March 1993."},{"issue":"2","key":"10.1016\/S0167-6423(99)00018-0_BIB38","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","article-title":"A practical decision procedure for arithmetic with function symbols","volume":"26","author":"Shostak","year":"1979","journal-title":"J. ACM"},{"key":"10.1016\/S0167-6423(99)00018-0_BIB39","unstructured":"T. Sreemani, J.M. Atlee, Feasibility of model checking software requirements, in: 11th Annual Conf. Computer Assurance COMPASS, June 1996, pp. 77\u201388."},{"key":"10.1016\/S0167-6423(99)00018-0_BIB40","doi-asserted-by":"crossref","unstructured":"P. Wolper, B. Boigelot, An automata theoretic approach to presburger arithmetic constraints, in: Proc. of Static Analysis Symp., Lecture Notes in Computer Science, vol. 983, Springer, Berlin, September 1995, pp. 21\u201332.","DOI":"10.1007\/3-540-60360-3_30"},{"issue":"2","key":"10.1016\/S0167-6423(99)00018-0_BIB41","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1145\/244795.244803","article-title":"Symbolic model checking for event-driven real-time systems","volume":"19","author":"Yang","year":"1997","journal-title":"ACM Trans. Programm. Lang. Systems"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642399000180?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642399000180?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,4]],"date-time":"2024-12-04T12:31:13Z","timestamp":1733315473000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642399000180"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,1]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,1]]}},"alternative-id":["S0167642399000180"],"URL":"https:\/\/doi.org\/10.1016\/s0167-6423(99)00018-0","relation":{},"ISSN":["0167-6423"],"issn-type":[{"type":"print","value":"0167-6423"}],"subject":[],"published":{"date-parts":[[2000,1]]}}}