Providing the shalls

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–107 (Jan. 1999)

Billings, C.: Aviation Automation: The Search for a Human-Centered Approach. Erlbaum, Mahwah, NJ (1997)

Brooks, F.: No silver bullet: essence and accidents of software engineering. IEEE Comput.20(4), 10–19 (1987)

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'98), vol. 1, pp. C41/1–C41/8. Belllevue, WA (Oct. 1998)

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–520 (1998)

Choi, Y.: Model checking RSML−e requirements. PhD Thesis, University of Minnesota (July 2003)

Choi, Y., Heimdahl, M.: Model checking RSML−e requirements. In: Proceedings of the 7th IEEE/IEICE International Symposium on High Assurance Systems Engineering, pp. 109–118. Tokyo (Oct. 2002)

Choi, Y., Rayadurgam, S., Heimdahl, M.: Toward automation for model checking requirement specifications with numeric constraints. Requir. Eng. J. 7(4), 225–242 (2002)

Davis, A.: Software Requirements: Object, Function, and States. Prentice-Hall, Englewood Cliffs, NJ (1993)

Fagan, M.: Design and code inspections to reduce errors in program development. IBM Syst. J. 15(3), 182–211 (1976)

Faulk, S., Brackett, J., Ward, P., Kirby, J.: The Core method for real-time requirements. IEEE Softw. 9(5), 22–33 (1992)

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–8. Gaithersburg, MD (June 1994)

Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Met. (TOSEM) 5(4), 293–333 (1996)

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–65 (March 1995)

Heitmeyer, C. Kirby, J., Labaw, B.: Automated consistency checking of requirements specification. ACM Trans. Softw. Eng. Methodol. (TOSEM) 5(3), 231–261 (1996)

Joshi, A., Miller, S., Heimdahl, M.: Mode confusion analysis of a flight guidance system using formal methods. In: 22nd Digital Avionics Systems Conference DASC'03, pp. 2.D.1–1–2.D.1–11 (Oct. 2003)

Leveson, N.: Safeware: system safety and computer. Addison-Wesley, Reading, MA (1995)

Leveson, N., Heimdahl, M., Hildreth, H., Reese, J.: Requirements specifications for process-control systems. IEEE Trans. Softw. Eng. 20(9), 684–707 (1994)

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)

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–145. Springer, Berlin Heidelberg New York (Sept. 1999)

Lutz, R.: Analyzing software requirements errors in safety-critical, embedded systems. In: IEEE Symposium on Requirements Engineering, pp. 126–133. San Diego (1993)

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–53. Clearwater Beach, FL (1998)

Miller, S., Tribble, A.: A methodology for improving mode awareness in flight guidance design. In: 21st Digital Avionics Systems Conference (DASC'02), vol. 2, pp. 7D1-1–7D1-11. Irvine, CA (Oct. 2002)

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

Owen, D., Menzies, T.: Lurch: a lightweight alternative to model checking. In: Proceedings of the 2003 Software Engineering and Knowledge Engineering Conference (SEKE'03), pp. 158–165 (2003)

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)

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–125 (1995)

Ramamoorthy, C., Prakesh, A., Tsai, W., Usuda, Y.: Software engineering: problems and perspectives. IEEE Comput. 17(10), 191–209 (1984)

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–186. Singapore (Nov. 2003)

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′99), Liege, Belgium (June 1999)

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-1–4.B.2-6. St. Louis, MO (Oct. 1999)

Sarter, N., Woods, D.: Pilot interaction with cockpit automation: operational experiences with the flight management system. Int. J. Aviat. Psychol. 2(4), 303–331 (1992)

Sarter, N., Woods, D.: Pilot interaction with cockpit automation II: an experimental study of pilots' model and awareness of the flight management system. Int. J. Aviat. Psychol.4(1), 1–28 (1994)

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–19 (1995)

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–179 (Sept. 1999)