Programming from Control Laws

点击翻译按钮获取中文摘要

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.