From owner-qed Tue Nov 1 10:31:49 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA01372 for qed-out; Tue, 1 Nov 1994 10:30:19 -0600 Received: from motgate.mot.com (motgate.mot.com [129.188.136.100]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA01367 for ; Tue, 1 Nov 1994 10:30:12 -0600 Received: from pobox.mot.com ([129.188.137.100]) by motgate.mot.com with SMTP (5.67b/IDA-1.4.4/MOT-3.1 for ) id AA08273; Tue, 1 Nov 1994 10:29:40 -0600 Received: from motgeg.geg.mot.com by pobox.mot.com with SMTP (5.67b/IDA-1.4.4/MOT-3.1 for ) id AA00688; Tue, 1 Nov 1994 10:24:39 -0600 Received: from csn1.geg.mot.com by motgeg.geg.mot.com (AIX 3.2/UCB 5.64/4.03) id AA25255; Tue, 1 Nov 1994 09:15:12 -0700 Received: from geglan.geg.mot.com by csn1.geg.mot.com (AIX 3.2/UCB 5.64/4.03) id AA11650; Tue, 1 Nov 1994 09:23:54 -0700 Received: by gegpo1.geg.mot.com with Microsoft Mail id <2EB66B2E@gegpo1.geg.mot.com>; Tue, 01 Nov 94 09:22:06 MST From: White Peter To: QED Cc: Scott William Subject: Who are the customers for QED. Date: Tue, 01 Nov 94 09:21:00 MST Message-Id: <2EB66B2E@gegpo1.geg.mot.com> Encoding: 61 TEXT X-Mailer: Microsoft Mail V3.0 Sender: owner-qed@mcs.anl.gov Precedence: bulk I would like to join the debate in a way that will vigorously stir the pot: When one wishes to plan a spaceflight for a planetary probe, the equations of motion for the planets, moons, and the probe are written down, constraints concerning the capabilities and objectives of the probe are written down, and the system is solved, yielding a mission plan that is optimal with respect to some objective function. Having generated the mission plan in this way, there is no question that the plan satisfies the laws of orbital mechanics. One does not generate a mission plan and then verify later that it satisfies the laws of orbital mechanics. Similarly one does not design an aircraft according to principles other than those of aerodynamics, and then later attempt to verify that it follows these principles. In the area of hardware and software development, one can either develop a system and then attempt to verify its correctness (post facto verification), or follow a path similar to the space probe mission plan (correctness by construction). Following correctness by construction, one might make specifications for the correct operation of the system, and then attempt to mathematically derive the implementation from the specification. There has been some research along these lines, including such languages as OBJ, CLEAR, and ML. What these have in common is that they rely heavily on a rather rich mathematical setting, namely category theory. There appears to be some sheaf theory creeping in as well. I am currently evaluating this correctness by construction technology to see if it is ready for practical application here at Motorola. With this as a background, I would like to state my positions on what QED could do for the industry: 1. I hope that the mathematical synthesis of hardware and software (correctness by construction) will become the method of choice for industry, over our traditional ad hoc methods, and over post facto verification. 2. I would like to execute correctness by construction in a rich mathematical environment. To take an extreme example, if I am developing software to control a particle accelerator, I might like to have all the mathematics necessary to do theoretical physics at my disposal, and not start out from set theory, with or without the axiom of choice. 3. I think the verification technology may be appropriate in establishing the soundness and/or consistency and/or correctness of the mathematical environment provided for me to do my correctness by construction. 4. I think that there may always be extremely low level components in hardware and software that are just too "grundgy" to do in a top down correctness by construction manner, and may have to be tackled with post facto verification. I think these woule be extremely small, isolated layers of a system. Many thanks for an interesting debate. Peter White, Motorola GSTG