{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:07:22Z","timestamp":1759032442062,"version":"3.32.0"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"4-5","license":[{"start":{"date-parts":[[2006,2,17]],"date-time":"2006-02-17T00:00:00Z","timestamp":1140134400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2006,8]]},"DOI":"10.1007\/s10009-004-0173-6","type":"journal-article","created":{"date-parts":[[2006,9,20]],"date-time":"2006-09-20T13:04:54Z","timestamp":1158757494000},"page":"303-319","source":"Crossref","is-referenced-by-count":48,"title":["Proving the shalls"],"prefix":"10.1007","volume":"8","author":[{"given":"Steven P.","family":"Miller","sequence":"first","affiliation":[]},{"given":"Alan C.","family":"Tribble","sequence":"additional","affiliation":[]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[]},{"given":"Mats P. E.","family":"Heimdahl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,2,17]]},"reference":[{"key":"173_CR1","unstructured":"Anonymous. Esterel Technologies Home Page. http:\/\/wwww.esterel-technologies.com"},{"key":"173_CR2","unstructured":"Anonymous. NASA Software Assurance Technology Center Formal Inspections Page. http:\/\/satc.gsfc.nasa.gov\/fi\/fipage.html"},{"key":"173_CR3","unstructured":"Anonymous. NuSMV Home Page. http:\/\/nusmv.irst.itc.it\/"},{"key":"173_CR4","unstructured":"Anonymous. PVS Home Page. http:\/\/www.csl.sri.com\/projects\/pvs"},{"key":"173_CR5","unstructured":"Anonymous. The MathWorks Home Page. http:\/\/wwww.mathworks.com"},{"key":"173_CR6","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Caspi, P., Parent-Vigouroux, C., Dumas, C.: A methodology for proving control systems with Lustre and PVS. In: Proceedings of the IEEE 7th Working Conference on Dependable Computing for Critical Applications (DCCA 7), San Jose, CA, pp. 89\u2013107 (Jan. 1999)","DOI":"10.1109\/DCFTS.1999.814291"},{"key":"173_CR7","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The synchronous programming lanugage esterel: design, semantics, and implementation. Sci. Comput. Prog. 19, 87\u2013152 (1992)","journal-title":"Sci. Comput. Prog."},{"key":"173_CR8","unstructured":"Billings, C.: Aviation Automation: The Search for a Human-Centered Approach. Erlbaum, Mahwah, NJ (1997)"},{"key":"173_CR9","unstructured":"Boehm, B.: Software Engineering Economics. Prentice-Hall, Englewood Cliffs, NJ (1981)"},{"issue":"4","key":"173_CR10","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1987.1663532","volume":"20","author":"F. Brooks","year":"1987","unstructured":"Brooks, F.: No silver bullet: essence and accidents of software engineering. IEEE Comput. 20(4), 10\u201319 (1987)","journal-title":"IEEE Comput."},{"key":"173_CR11","doi-asserted-by":"crossref","unstructured":"Butler, R., Miller, S., Potts, J., Carreno, V.: A formal methods approach to the analysis of mode confusion. In: 17th Digital Avionics Systems Conference (DASC\u2019 98), vol. 1, pp. C41\/1\u2013C41\/8. Belllevue, WA (Oct. 1998)","DOI":"10.1109\/DASC.1998.741497"},{"issue":"7","key":"173_CR12","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W. Chan","year":"1998","unstructured":"Chan, W., Anderson, R., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.: Model checking large software specifications. IEEE Trans. Softw. Eng. 24(7), 498\u2013520 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"173_CR13","unstructured":"Choi, Y.: Model checking RSML\u2212e requirements. PhD Thesis, University of Minnesota (July 2003)"},{"key":"173_CR14","unstructured":"Choi, Y., Heimdahl, M.: Model checking RSMLe requirements. In: Proceedings of the 7th IEEE\/IEICE International Symposium on High Assurance Systems Engineering, pp. 109\u2013118. Tokyo (Oct. 2002)"},{"issue":"4","key":"173_CR15","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/s007660200018","volume":"7","author":"Y. Choi","year":"2002","unstructured":"Choi, Y., Rayadurgam, S., Heimdahl, M.: Toward automation for model checking requirement specifications with numeric constraints. Requir. Eng. J. 7(4), 225\u2013242 (2002)","journal-title":"Requir. Eng. J."},{"key":"173_CR16","volume-title":"Model Checking","author":"E. Clark","year":"2001","unstructured":"Clark, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA (2001)"},{"key":"173_CR17","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, NJ (1993)"},{"key":"173_CR18","unstructured":"de Moura, L.: SAL: Tutorial. SRI International, Computer Science Laboratory. Menlo Park, CA (Jan. 2004)"},{"issue":"3","key":"173_CR19","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1147\/sj.153.0182","volume":"15","author":"M. Fagan","year":"1976","unstructured":"Fagan, M.: Design and code inspections to reduce errors in program development. IBM Syst. J. 15(3), 182\u2013211 (1976)","journal-title":"IBM Syst. J."},{"issue":"5","key":"173_CR20","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1109\/52.156894","volume":"9","author":"S. Faulk","year":"1992","unstructured":"Faulk, S., Brackett, J., Ward, P., Kirby, J.: The Core method for real-time requirements. IEEE Softw. 9(5), 22\u201333 (1992)","journal-title":"IEEE Softw."},{"key":"173_CR21","doi-asserted-by":"crossref","unstructured":"Faulk, S., Finneran, L., Kirby, J., Shah, S., Sutton, J.: Experience applying the Core method to the Lockheed C-130J software requirements. In: 9th Annual Conference on Computer Assurance, pp. 3\u20138. Gaithersburg, MD (June 1994)","DOI":"10.1109\/CMPASS.1994.318472"},{"issue":"4","key":"173_CR22","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D. Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Met. (TOSEM) 5(4), 293\u2013333 (1996)","journal-title":"ACM Trans. Softw. Eng. Met. (TOSEM)."},{"key":"173_CR23","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C., Labaw, B., Kiskis, D.: Consistency checking of SCR-style requirements specifications. In: Proceedings of the 2nd IEEE International Symposium on Requirements Engineering, pp. 56\u201365 (March 1995)","DOI":"10.1109\/ISRE.1995.512546"},{"issue":"3","key":"173_CR24","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C. Heitmeyer","year":"1996","unstructured":"Heitmeyer, C. Kirby, J., Labaw, B.: Automated consistency checking of requirements specification. ACM Trans. Softw. Eng. Methodol. (TOSEM) 5(3), 231\u2013261 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)."},{"key":"173_CR25","doi-asserted-by":"crossref","unstructured":"Joshi, A., Miller, S., Heimdahl, M.: Mode confusion analysis of a flight guidance system using formal methods. In: 22nd Digital Avionics Systems Conference DASC\u201903, pp. 2.D.1\u20131\u20132.D.1\u201311 (Oct. 2003)","DOI":"10.1109\/DASC.2003.1245813"},{"key":"173_CR26","volume-title":"Safeware: system safety and computer","author":"N. Leveson","year":"1995","unstructured":"Leveson, N.: Safeware: system safety and computer. Addison-Wesley, Reading, MA (1995)"},{"key":"173_CR27","unstructured":"Leveson, N., Heimdahl, M., Hildreth, H., Reese, J.: TCAS II Collision Avoidance System (CAS) System Requirements Specification change 6.00. Federal Aviation Administration, U.S. Department of Transportation (1993)"},{"issue":"9","key":"173_CR28","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"N. Leveson","year":"1994","unstructured":"Leveson, N., Heimdahl, M., Hildreth, H., Reese, J.: Requirements specifications for process-control systems. IEEE Trans. Softw. Eng. 20(9), 684\u2013707 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"173_CR29","unstructured":"Leveson, N., Pinnel, D., Sandys, S., Koga, S., Reese, J.: Analyzing software specifications for mode confusion potential. In: Workshop on Human Error and System Development, Glasgow, UK (March 1997)"},{"key":"173_CR30","doi-asserted-by":"crossref","unstructured":"Leveson, N., Heimdahl, M., Reese, J.: Designing specification languages for process control systems: Lessons learned and steps to the future. In: 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Lecture Notes in Computer Science, vol. 1687, pp. 127\u2013145. Springer, Berlin Heidelberg New York (Sept. 1999)","DOI":"10.1145\/318774.318937"},{"key":"173_CR31","doi-asserted-by":"crossref","unstructured":"Lutz, R.: Analyzing software requirements errors in safety-critical, embedded systems. In: IEEE Symposium on Requirements Engineering, pp. 126\u2013133. San Diego (1993)","DOI":"10.1109\/ISRE.1993.324825"},{"key":"173_CR32","doi-asserted-by":"crossref","unstructured":"Miller, S.: Specifying the mode logic of a flight guidance system in CoRE and SCR. In: 2nd Workshop on Formal Methods in Software Practice (FMSP98), pp 44\u201353. Clearwater Beach, FL (1998)","DOI":"10.1145\/298595.298856"},{"key":"173_CR33","unstructured":"Miller, S.: Taxonomy of mode confusion sources\u2014final report. In: NASA Contractor Report (Feb. 2001)"},{"key":"173_CR34","doi-asserted-by":"crossref","unstructured":"Miller, S., Tribble, A.: A methodology for improving mode awareness in flight guidance design. In: 21st Digital Avionics Systems Conference (DASC\u201902), vol. 2, pp. 7D1\u20131\u20137D1\u201311. Irvine, CA (Oct. 2002)","DOI":"10.1109\/DASC.2002.1052928"},{"key":"173_CR35","unstructured":"Miller, S., Tribble, A., Carlson, T., Danielson, E.: Flight guidance system requirements specification. Technical Report CR-2003-212426, NASA Langley Research Center (June 2003). http:\/\/techreports.larc.nasa.gov\/ltrs\/refer\/2003\/cr\/NASA-2003-cr212426.refer.html"},{"key":"173_CR36","unstructured":"Owen, D., Menzies, T.: Lurch: a lightweight alternative to model checking. In: Proceedings of the 2003 Software Engineering and Knowledge Engineering Conference (SEKE\u201903), pp. 158\u2013165 (2003)"},{"key":"173_CR37","unstructured":"Owre, S., Rushby, J., Shankar, N.: Analyzing tabular and state-transition requirements specifications in PVS. Technical Report SRI-CSL-95-12, SRI International, Menlo Park, CA (June 1995)"},{"issue":"2","key":"173_CR38","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Owre, S., Rushby, J., Shankar, N., Henke, F.: Formal verification for fault-tolerant architectures: prolegomena to the design of PVS. IEEE Trans. Softw. Eng. 21(2), 107\u2013125 (1995)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"173_CR39","unstructured":"Parnas, D., Madey, J.: Functional documentation for computer systems engineering (vol. 2). Technical Report CRL 237, McMaster University, Hamilton, Ontario, Canada (Sept. 1990)"},{"issue":"10","key":"173_CR40","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1109\/MC.1984.1658970","volume":"17","author":"C. Ramamoorthy","year":"1984","unstructured":"Ramamoorthy, C., Prakesh, A., Tsai, W., Usuda, Y.: Software engineering: problems and perspectives. IEEE Comput. 17(10), 191\u2013209 (1984)","journal-title":"IEEE Comput."},{"key":"173_CR41","doi-asserted-by":"crossref","unstructured":"Rayadurgam, S., Joshi, A., Heimdahl, M.: Using PVS to prove properties of systems modelled in a synchronous dataflow language. In: Proceedigns of the 5th International Conference on Formal Engineering Methods (ICFEM 2003), pp. 167\u2013186. Singapore (Nov. 2003)","DOI":"10.1007\/978-3-540-39893-6_11"},{"key":"173_CR42","unstructured":"Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. In: Proceedings of the 3rd Workshop on Human Error, Safety, and System Development (HESSD\u201999), Liege, Belgium (June 1999)"},{"key":"173_CR43","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Analyzing cockpit interfaces using formal models. Electron. Notes Theor. Comput. Sci. 43, 1\u201314 (2001)","DOI":"10.1016\/S1571-0661(04)80891-0"},{"key":"173_CR44","doi-asserted-by":"crossref","unstructured":"Rushby, J., Crow, J., Palmer, E.: An automated method to detect potential mode confusion. In: Proceedings of the 18th AIAA\/IEEE Digital Avionics Systems Conference (DASC), vol. 1, pp. 4.B.2\u20131\u20134.B.2\u20136. St. Louis, MO (Oct. 1999)","DOI":"10.1109\/DASC.1999.863725"},{"issue":"4","key":"173_CR45","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1207\/s15327108ijap0204_5","volume":"2","author":"N. Sarter","year":"1992","unstructured":"Sarter, N., Woods, D.: Pilot interaction with cockpit automation: operational experiences with the flight management system. Int. J. Aviat. Psychol. 2(4), 303\u2013331 (1992)","journal-title":"Int. J. Aviat. Psychol."},{"issue":"1","key":"173_CR46","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1207\/s15327108ijap0401_1","volume":"4","author":"N. Sarter","year":"1994","unstructured":"Sarter, N., Woods, D.: Pilot interaction with cockpit automation II: an experimental study of pilots\u2019 model and awareness of the flight management system. Int. J. Aviat. Psychol. 4(1), 1\u201328 (1994)","journal-title":"Int. J. Aviat. Psychol."},{"issue":"1","key":"173_CR47","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1518\/001872095779049516","volume":"37","author":"N. Sarter","year":"1995","unstructured":"Sarter, N., Woods, D.: How in the world did I ever get into that mode?: mode error and awareness in supervisory control. Hum. Fact. 37(1), 5\u201319 (1995)","journal-title":"Hum. Fact."},{"key":"173_CR48","doi-asserted-by":"crossref","unstructured":"Thompson, J., Heimdahl, M., Miller, S.: Specification based prototyping for embedded systems. In: 7th ACM SIGSOFT Symposium on the Foundations on Software Engineering, Lecture Notes in Computer Science, vol 1687, pp. 163\u2013179 (Sept. 1999)","DOI":"10.1007\/3-540-48166-4_11"},{"key":"173_CR49","doi-asserted-by":"crossref","unstructured":"Tribble, A., Miller, S.: Safety analysis of a flight guidance system. In: 21st Digital Avionics Systems Conference (DASC\u201902), vol. 2, pp. 13C1\u20131\u201313C1\u201310. Irvine, CA (Oct. 2002)","DOI":"10.1109\/DASC.2002.1053007"},{"key":"173_CR50","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, Canada (1990)"},{"key":"173_CR51","unstructured":"Whalen, M.W.: A formal semantics for RSML\u2212e . Master\u2019s thesis, University of Minnesota (May 2000)"},{"key":"173_CR52","unstructured":"Whalen, M.W.: Trustworthy translation for RSML\u2212e . PhD thesis, University of Minnesota (Dec. 2004)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0173-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0173-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0173-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T23:07:03Z","timestamp":1736550423000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0173-6"}},"subtitle":["Early validation of requirements through formal methods"],"short-title":[],"issued":{"date-parts":[[2006,2,17]]},"references-count":52,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2006,8]]}},"alternative-id":["173"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0173-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2006,2,17]]}}}