{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:34:38Z","timestamp":1773192878275,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540408284","type":"print"},{"value":"9783540452362","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45236-2_6","type":"book-chapter","created":{"date-parts":[[2010,6,26]],"date-time":"2010-06-26T00:08:38Z","timestamp":1277510918000},"page":"75-93","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Proving the Shalls"],"prefix":"10.1007","author":[{"given":"Steven P.","family":"Miller","sequence":"first","affiliation":[]},{"given":"Alan C.","family":"Tribble","sequence":"additional","affiliation":[]},{"given":"Mats P. E.","family":"Heimdahl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,9,25]]},"reference":[{"key":"6_CR1","volume-title":"No Silver Bullet: Essence and Accidents of Software Engineering","author":"F. Brooks","year":"1987","unstructured":"Brooks, F.: No Silver Bullet: Essence and Accidents of Software Engineering. IEEE Computer, Los Alamitos (April 1987)"},{"key":"6_CR2","volume-title":"Software Engineering Economics","author":"B. Boehm","year":"1981","unstructured":"Boehm, B.: Software Engineering Economics. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"6_CR3","volume-title":"Software Requirements (Revised): Object, Functions, and States","author":"A. Davis","year":"1993","unstructured":"Davis, A.: Software Requirements (Revised): Object, Functions, and States. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"6_CR4","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)"},{"key":"6_CR5","first-page":"191","volume-title":"Software Engineering: Problems and Perspectives","author":"C. Ramamoorthy","year":"1984","unstructured":"Ramamoorthy, C., Prakesh, A., Tsai, W., Usuda, Y.: Software Engineering: Problems and Perspectives, October 1984, pp. 191\u2013209. IEEE Computer, Los Alamitos (1984)"},{"key":"6_CR6","volume-title":"Safeware: System Safety and Computers","author":"N. Leveson","year":"1995","unstructured":"Leveson, N.: Safeware: System Safety and Computers. Addison-Wesley Publishing Company, Reading (1995)"},{"key":"6_CR7","unstructured":"Lutz, R.: Analyzing Software Requirements Errors in Safety-Critical, Embedded, Systems. In: IEEE International Symposium on Requirements Engineering, San Diego, CA (January 1993)"},{"issue":"3","key":"6_CR8","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C. Heitmeyer","year":"1996","unstructured":"Heitmeyer, C., Jeffords, R., Labaw, B.: Automated Consistency Checking of Requirements Specification. ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a05(3), 231\u2013261 (1996)","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"6_CR9","unstructured":"Parnas, D., Madey, J.: Functional Documentation for Computer Systems Engineering (Vol. 2), Technical Report CRL 237, McMaster University, Hamilton, Ontario (September 1991)"},{"issue":"5","key":"6_CR10","doi-asserted-by":"publisher","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 Software\u00a09(5), 22\u201333 (1992)","journal-title":"IEEE Software"},{"key":"6_CR11","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: Proceedings of the Ninth Annual Conference on Computer Assurance, Gaithersburg, MD, June 1994, pp. 3\u20138 (1994)","DOI":"10.1109\/CMPASS.1994.318472"},{"issue":"9","key":"6_CR12","doi-asserted-by":"publisher","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 Transactions on Software Engineering\u00a020(9), 684\u2013707 (1994)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"6_CR13","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"H. Harel","year":"1996","unstructured":"Harel, H., Naamad, A.: The STATEMATE Semantics of Statecharts. ACM Transactions on Software Engineering and Methodology\u00a05(4), 293\u2013333 (1996)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Miller, S.: Specifying the Mode Logic of a Flight Guidance System in CoRE and SCR. In: Proceedings of The Second Annual Workshop on Formal Methods in Software Practice (FMSP 1998), Clearwater Beach, Florida, March 4-5 (1998)","DOI":"10.1145\/298595.298856"},{"key":"6_CR15","unstructured":"Butler, R., Miller, S., Potts, J., Carreno, V.: A Formal Methods Approach to the Analysis of Mode Confusion. In: Proceedings of the 17th AIAA\/IEEE Digital Avionics Systems Conference, Bellevue, WA (October 1998)"},{"key":"6_CR16","unstructured":"Miller, S., Tribble, A.: A Methodology for Improving Mode Awareness in Flight Guidance Design. In: Proceedings of the 21st Digital Avionics Systems Conference (DASC 2002), Irvine, CA (October 2002)"},{"key":"6_CR17","unstructured":"Tribble, A., Lempia, D., Miller, S.: Software Safety Analysis of a Flight Guidance System. In: Proceedings of the 21st Digital Avionics Systems Conference (DASC 2002), Irvine, CA (October 2002)"},{"key":"6_CR18","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. Thompson","year":"1999","unstructured":"Thompson, J., Heimdahl, M., Miller, S.: Specification Based Prototyping for Embedded Systems. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol.\u00a01687, p. 163. Springer, Heidelberg (1999)"},{"key":"6_CR19","doi-asserted-by":"publisher","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. Science of Computer Programming\u00a019, 87\u2013152 (1992)","journal-title":"Science of Computer Programming"},{"key":"6_CR20","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. Thompson","year":"1999","unstructured":"Thompson, J., Heimdahl, M., Miller, S.: Specification Based Prototyping for Embedded Systems. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol.\u00a01687, p. 163. Springer, Heidelberg (1999)"},{"key":"6_CR21","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Grumberg, O., Peled, P.: Model Checking. The MIT Press, Cambridge (2001)"},{"key":"6_CR22","unstructured":"Anonymous, NuSMV Home Page, http:\/\/nusmv.irst.itc.it\/"},{"issue":"2","key":"6_CR23","doi-asserted-by":"publisher","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 Transactions on Software Engineering\u00a021(2), 107\u2013125 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR24","unstructured":"Anonymous, PVS Home Page, http:\/\/www.csl.sri.com\/projects\/pvs\/"},{"key":"6_CR25","unstructured":"Miller, S., Tribble, A., Carlson, T., Danielson, E.: Flight Guidance System Requirements Specification Final Report, NASA Contractor Report (November 2001)"},{"key":"6_CR26","unstructured":"Heimdahl, M., Rayadurgam, S., Choi, Y., Joshi, A., Devaraj, G.: Proof and Model Checking Tools Final Report, NASA Contractor Report (November 2002)"},{"key":"6_CR27","unstructured":"Tribble, A.: FGS Safety Analysis Final Report, NASA Contractor Report (November 2002)"},{"key":"6_CR28","unstructured":"Billings, C.: Aviation Automation: the Search for a Human Centered Approach. Lawrence Erlbaum Associates, Inc., Mahwah (1997)"},{"issue":"4","key":"6_CR29","doi-asserted-by":"publisher","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. The International Journal of Aviation Psychology\u00a02(4), 303\u2013331 (1992)","journal-title":"The International Journal of Aviation Psychology"},{"issue":"1","key":"6_CR30","doi-asserted-by":"publisher","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. The International Journal of Aviation Psychology\u00a04(1), 1\u201328 (1994)","journal-title":"The International Journal of Aviation Psychology"},{"issue":"1","key":"6_CR31","first-page":"5","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, Human Factors\u00a037(1), 5\u201319 (1995)","journal-title":"Mode Error and Awareness in Supervisory Control, Human Factors"},{"key":"6_CR32","unstructured":"Miller, S.: Taxonomy of Mode Confusion Sources Final Report, NASA Contractor Report (February 2001)"},{"key":"6_CR33","unstructured":"Leveson, N., et al.: Analyzing Software Specifications for Mode Confusion Potential. In: Johnson, C.W. (ed.) Proceedings of a Workshop on Human Error and System Development, Glasgow, Scotland, March 1997, pp. 132\u2013146 (1997)"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Analyzing Cockpit Interfaces Using Formal Methods. Electronic Notes in Theoretical Computer Science\u00a043 (2001), URL: http:\/\/wwww.elsevier.nl\/locate\/entcs\/volume43.html","DOI":"10.1016\/S1571-0661(04)80891-0"},{"key":"6_CR35","unstructured":"Rushby, J.: Using Model Checking to Help Discover Mode Confusions and Other Automation Surprises. In: The Proceedings of the 3rd Workshop on Human Error, Safety, and System Development (HESSD 1999), Liege, Belgium, June 7-8 (1999)"},{"key":"6_CR36","unstructured":"Rushby, J., Crow, J., Palmer, E.: An Automated Method to Detect Potential Mode Confusion. In: The Proceedings of the 18th AIAA\/IEEE Digital Avionics Systems Conference (DASC), St. Louis, MO (October 1999)"},{"key":"6_CR37","unstructured":"Miller, S., Joshi, A.: FGS Mode Awareness Final Report, NASA Contractor Report (November 2002)"}],"container-title":["Lecture Notes in Computer Science","FME 2003: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45236-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T08:02:36Z","timestamp":1740211356000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45236-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408284","9783540452362"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45236-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"25 September 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}