Automated decision in transportation and medical systems is a growing part of our daily lives. During this process, human responsibility for vehicle or medical safety shifts from that of the operator to that of the off-board, off-line design engineer and his employer. Historically, the link between system accident and operator responsibility is very strong, as many system malfunctions have been traced, for valid or invalid reasons, to human operator malfunction. The link between system accident, decision software malfunction, and software design engineering responsibility is much weaker and more diffuse. As a result, there is a strong desire for automated decision-making to offer fully-guaranteed behavior prior to vehicle operation.

 

As vehicles grow in complexity and autonomy, the need for certification becomes more urgent and, unfortunately, much more difficult to achieve due to software length and decision-making complexity. We argue that generic software analysis methods can only verify low-level software properties, and that domain-specific knowledge must be used to validate the software against its specifications. We illustrate this point by introducing credible autocoding, a software design approach that generates control and optimization software interlaced with formal semantics describing high-level system properties and their proof. The choice of applications to control and optimization is motivated by their significant relevance to current and future automated decision-making tools.

 

Eric Feron is Dutton/Ducoffe professor of aerospace software engineering at Georgia Tech, and consulting professor of applied mathematics at Ecole Nationale de l'Aviation Civile. He is interested in all aspects of decision making as they arise in aerospace applications