Proofreading CPS

Cyber-physical systems (CPS) encompasses all instances of interaction between a physical object and some computational portion of that object in the modern world. A specific example of a CPS would be the interaction between an airplane and its collision detection system.

As with any piece of computer software, a given design with an apparent flaw will ideally be fixed to working order in while still in the design stage. If the flaws proceed into the manufacturing state, then the only way to find those flaws would be to employ trial-and-error. In the case of an airplane collision detection system, such trials would be expensive, time-consuming and ultimately impractical.

A research team at Carnegie Mellon have developed a piece of software that, provided with some initial parameters, will attempt to find a counterexample which illustrates a flaw in a given design. For example, an airplane on a collision course with another airplane will recieve evasion instructions from its collision detection system in order to avoid a universally fatal plane crash. The software, after recieving the parameters of the collision detection system, will attempt to find a scenario where the two planes will crash into each other.

Employing typical "brute-force" methods to this problem would be a computational nightmare, if not outright impossible. This is due to the infinitely many variables present in the real world that can affect the outcome of the system. The method employed in the software attempts to bypass this difficulty by extrapolating "differential invariants", or basic pieces of the problem that never change regardless of the variables. Using the many differential invariants in the collision problem, the software will attempt to piece together a counterexample or prove that the design is sound when no such counterexample can exist.

The latter is obviously the difficult part.

Method For Verifying Safety Of Computer-controlled Devices Developed [Science Daily]