{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:47Z","timestamp":1725516527290},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_42","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"392-402","source":"Crossref","is-referenced-by-count":2,"title":["A Case for Specification Validation"],"prefix":"10.1007","author":[{"given":"Mats P. E.","family":"Heimdahl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"42_CR1","unstructured":"Archer, M., Heitmeyer, C., Sims, S.: TAME: A PVS interface to simplify proofs for automata models. In: User Interfaces for Theorem Provers (1998)"},{"key":"42_CR2","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1109\/DCFTS.1999.814291","volume-title":"Proceedings of the Seventh Working Conference on Dependable Computing for Critical Applications (DCCA 7)","author":"S. Bensalem","year":"1999","unstructured":"Bensalem, S., Caspi, P., Parent-Vigouroux, C., Dumas, C.: A methodology for proving control systems with Lustre and PVS. In: Proceedings of the Seventh Working Conference on Dependable Computing for Critical Applications (DCCA 7), San Jose CA, January 1999, pp. 89\u2013107. IEEE Computer Society Press, Los Alamitos (1999)"},{"issue":"5","key":"42_CR3","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1109\/32.232011","volume":"19","author":"B.L. Valdis","year":"1993","unstructured":"Valdis, B.L., Yehudai, A.: Using transformations in specification-based prototyping. IEEE Transactions on Software Engineering\u00a019(5), 436\u2013452 (1993)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"42_CR4","doi-asserted-by":"crossref","unstructured":"Blackburn, M.R., Busser, R.D., Fontaine, J.S.: Automatic generation of test vectors for SCR-style specifications. In: Proceedings of the 12th Annual Conference on Computer Assurance, COMPASS 1997 (June 1997)","DOI":"10.1109\/CMPASS.1997.613225"},{"key":"42_CR5","volume-title":"Software Engineering Economics","author":"B. Boehm","year":"1981","unstructured":"Boehm, B.: Software Engineering Economics. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"42_CR6","doi-asserted-by":"crossref","unstructured":"Brooks, F.: No silver bullet: Essence and accidents of software engineering. IEEE Computer, 10\u201319 (April 1997)","DOI":"10.1109\/MC.1987.1663532"},{"key":"42_CR7","doi-asserted-by":"crossref","unstructured":"Butler, R., Miller, S., Potts, J., Carreno, V.: A formal methods approach to the analysis of mode confusion. In: 17st Digital Avionics Systems Conference (DASC 1998), Belllevue, WA, pp. C41\/1 \u2013 C41\/8 (October 1998)","DOI":"10.1109\/DASC.1998.741497"},{"key":"42_CR8","unstructured":"Callahan, J., Schneider, F., Easterbrook, S.: Specification-based testing using model checking. In: Proceedings of the SPIN Workshop (August 1996)"},{"issue":"7","key":"42_CR9","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W. Chan","year":"1998","unstructured":"Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.D.: Model checking large software specifications. IEEE Transactions on Software Engineering\u00a024(7), 498\u2013520 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"42_CR10","unstructured":"Choi, Y., Heimdahl, M.: Model checking RSML\u2212\u2009e requirements. In: Proceedings of the 7th IEEE\/IEICE International Symposium on High Assurance Systems Engineering, Tokyo, Japan, October 2002, pp. 109\u2013118 (2002)"},{"key":"42_CR11","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"42_CR12","volume-title":"Software Requirements: Object, Function, and States","author":"A. Davis","year":"1993","unstructured":"Davis, A.: Software Requirements: Object, Function, and States. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"42_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/BFb0035401","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Engels","year":"1997","unstructured":"Engels, A., Feijs, L.M.G., Mauw, S.: Test generation for intelligent networks using model checking. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 384\u2013398. Springer, Heidelberg (1997)"},{"issue":"6","key":"42_CR14","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1145\/318774.318939","volume":"24","author":"A. Gargantini","year":"1999","unstructured":"Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. Software Engineering Notes\u00a024(6), 146\u2013162 (1999)","journal-title":"Software Engineering Notes"},{"issue":"3","key":"42_CR15","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"42_CR16","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., Trakhtenbrot, M.: Statemate: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering\u00a016(4), 403\u2013414 (1990)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"6","key":"42_CR17","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1109\/32.508311","volume":"22","author":"M.P.E. Heimdahl","year":"1996","unstructured":"Heimdahl, M.P.E., Leveson, N.G.: Completeness and consistency in hierarchical state-base requirements. IEEE Transactions on Software Engineering\u00a022(6), 363\u2013377 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"42_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Recent Trends in Data Type Specification","author":"C. Heitmeyer","year":"1996","unstructured":"Heitmeyer, C., Bull, A., Gasarch, C., Labaw, B.: SCR*: A toolset for specifying and analyzing requirements. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol.\u00a01130, Springer, Heidelberg (1996)"},{"issue":"3","key":"42_CR19","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C.L. Heitmeyer","year":"1996","unstructured":"Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology\u00a05(3), 231\u2013261 (1996)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"11","key":"42_CR20","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C. Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Kirby Jr., J., Labaw, B., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering\u00a024(11), 927\u2013948 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"42_CR21","doi-asserted-by":"crossref","unstructured":"Jasper, R., Brennan, M., Williamson, K., Currier, B., Zimmerman, D.: Test data generation and feasible path analysis. In: Proc. of Int\u2019l Symp. on Software Testing and Analysis, August 1994, pp. 95\u2013107 (1994)","DOI":"10.1145\/186258.187150"},{"key":"42_CR22","doi-asserted-by":"crossref","unstructured":"Joshi, A., Miller, S.P., Heimdahl, M.P.E.: Mode confusion analysis of a flight guidance system using formal methods. In: 22nd Digital Avionics Systems Conference (DASC 2003), pp. 2.D.1\u20131 \u2013 2.D.1\u201311(October 2003)","DOI":"10.1109\/DASC.2003.1245813"},{"key":"42_CR23","unstructured":"Lee, E.A.: Overview of the ptolemy project. Technical Report Technical Memorandum UCB\/ERL M03\/25, University of California, Berkeley, CA, 94720, USA (July 2003)"},{"key":"42_CR24","volume-title":"Safeware: System Safety and Computer","author":"N. Leveson","year":"1995","unstructured":"Leveson, N.: Safeware: System Safety and Computer. Addison-Wesley, Reading (1995)"},{"key":"42_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-48166-4_9","volume-title":"Software Engineering - ESEC\/FSE \u201999","author":"N.G. Leveson","year":"1999","unstructured":"Leveson, N.G., Heimdahl, M.P.E., Reese, J.D.: Designing Specification Languages for Process Control Systems: Lessons Learned and Steps to the Future. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol.\u00a01687, pp. 127\u2013145. Springer, Heidelberg (1999)"},{"key":"42_CR26","unstructured":"Lutz, R.: An overview of REFINE 2.0. In: Proceedings of the First ACM SIGSOFT Symposium on the Foundations of Software Engineering (1993)"},{"key":"42_CR27","unstructured":"Miller, S., Tribble, A., Carlson, T., Danielson, E.: Flight guidance system requirements specification. Technical Report CR-, -212426, NASA Langley Research Center (June 2003), http:\/\/techreports.larc.nasa.gov\/ltrs\/refer\/2003\/cr\/NASA-2003-cr212426.refer"},{"key":"42_CR28","doi-asserted-by":"crossref","unstructured":"Offutt, A.J., Xiong, Y., Liu, S.: Criteria for generating specification-based tests. In: Proceedings of the Fifth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 1999) (October 1999)","DOI":"10.1109\/ICECCS.1999.802856"},{"key":"42_CR29","doi-asserted-by":"crossref","unstructured":"Ramamoorthy, C., Prakesh, A., Tsai, W., Usuda, Y.: Software engineering: Problems and perspectives. IEEE Computer, 191\u2013209 (October 1984)","DOI":"10.1109\/MC.1984.1658970"},{"key":"42_CR30","volume-title":"Proceedings of the 8th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2001)","author":"S. Rayadurgam","year":"2001","unstructured":"Rayadurgam, S., Heimdahl, M.P.E.: Coverage based test-case generation using model checkers. In: Proceedings of the 8th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2001), April 2001, IEEE Computer Society, Los Alamitos (2001)"},{"key":"42_CR31","unstructured":"RTCA. Software Consideration. In: Airborne Systems and Equipment Certification. RTCA (1992)"},{"key":"42_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/3-540-48166-4_11","volume-title":"Software Engineering - ESEC\/FSE \u201999","author":"J.M. Thompson","year":"1999","unstructured":"Thompson, J.M., Heimdahl, M.P.E., Miller, S.P.: Specification based prototyping for embedded systems. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol.\u00a01687, pp. 163\u2013179. Springer, Heidelberg (1999)"},{"key":"42_CR33","doi-asserted-by":"crossref","unstructured":"Tribble, A., Miller, S.: Safety analysis of a flight guidance system. In: 21st Digital Avionics Systems Conference (DASC 2002), Irvine, CA, October 2002, vol.\u00a02, pp. 13C1\u20131 \u2013 13C1\u201310 (2002)","DOI":"10.1109\/DASC.2002.1053007"},{"key":"42_CR34","unstructured":"van Schouwen, A.: The A-7 requirements model: Re-examination for real-time systems and an application to monitoring systems. Technical Report 90-276, Queens University, Hamilton, Ontario (1990)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:43:56Z","timestamp":1557719036000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}