Programming from Control Laws

如今，计算机和计算机程序的使用非常普遍，但每个计算机用户都知道程序会出错。虽然当我们最喜欢的文本编辑器丢失了一点我们的工作时，这只是令人讨厌的，但当一个计算机程序（例如，控制飞机部件）出错时，后果可能会严重得多。为了开发这种应用程序，英国政府制定了需要使用特殊技术的指导方针。任何人都可以开发和销售文本编辑器，但如果程序失败会危及生命，则需要得到有关当局的认证。工程师使用一种称为控制律图的图形符号来指定控制应用。通常情况下，它们是由专门的设备与程序相结合来实现的。需要投入大量的精力来确保程序是正确的，因此是可认证的。最广泛使用的认证技术是测试。这需要程序运行多次，以尝试覆盖其所有可能的用途。QinetiQ是一家英国公司;他们是欧洲最大的科学和技术组织。他们设计了一种更便宜的方法来证明控制程序的正确性。他们使用数学符号和强大的计算机工具来确定程序满足控制律图中指定的所有要求。在这个项目中，我们建议通过将成熟的编程技术从规范应用到这个新领域来进一步发展他们的想法。我们需要的是一种根据控制律图进行编程的技术。我们的挑战是提供一种由工具支持的专业技术，允许程序员忽略所涉及的数学理论。控制系统是航空电子、汽车和电力等领域的关键。该项目将通过皇家学会工业奖学金与QinetiQ进行持续合作。这种与工业界的密切联系将保证我们的结果是相关的。QinetiQ的经验表明，认证成本可能降低2.5至4.5倍。

The use of computers and computer programs is pervasive nowadays, but every computer user knows that programs go wrong. While it is just annoying when our favourite text editor looses a bit of our work, the consequences are potentially much more serious when a computer program which, for instance, controls parts of an airplane goes wrong. To develop this sort of application, the UK government has produced guidelines which require the use of special techniques. Anybody can develop and sell a text editor, but programs whose failure can endanger lives need to be certified by the proper authorities. Engineers use a graphical notation called control law diagrams to specify control applications. Typically, they are implemented by specialised pieces of equipment in conjunction with programs. A lot of effort needs to be put into assuring that the programs are correct and, therefore, certifiable. The most widely used technique for certification is testing. This requires that the program is run several times, in an attempt to cover all its possible uses. QinetiQ is a British company; they are Europe's largest science and technology organisation. They have devised a much cheaper way of providing evidence of the correctness of control programs. They use mathematical notations and powerful computer tools to establish that the programs satisfy all the requirements specified in a control law diagram. In this project, we propose to further develop their ideas by applying well-established techniques of programming from specifications to this novel area. What we want is a technique for programming from control law diagrams. Our challenge is to provide a specialised technique, supported by tools, that allows programmers to ignore the mathematical theory involved. Control systems are key in the avionics, automotive, and power sectors, among others.The project will be part of an ongoing collaboration with QinetiQ through a Royal Society Industry Fellowship. This close contact with industry will guarantee that our results are relevant. Experience at QinetiQ shows a potential reduction factor of two and a half to four and half in the cost of certification.