Proving Cyber-Physical Systems Correct
Every branch of engineering applies mathematics to reliably-control its subject, except Software Engineering; rarely are programs, their specifications, and their executions treated as mathematical objects. They should be. Therefore, programs must be expressed in a language that is completely, mathematically defined. Furthermore, the language must usefully, and accurately define semantics for specifications and executions such that proofs that every execution of a programs meets its specification, may be constructed and exhibited. Programs for embedded systems (a.k.a. firmware) are even more challenging because firmware must exhibit timing behavior crucial to the system's operation, in addition to mere computation. For this purpose, the Behavioral Language for Embedded Systems with Software (BLESS) was created to be an annex sublanguage of the Architecture Analysis and Design Language (AADL). Mr. Larson's presentation will survey current medical device industry systems/firmware development practices, explain how AADL architectures augmented with BLESS behaviors allows safety-critical systems to be proved correct, demonstrate the BLESS proof tool being developed, and look at a formal proof of thread behavior emitted when proof-checking passes.
Brian Larson is a principal at the Multitude Corporation and an active member of the AADL standard committee (SAE AS5506A). He holds BSEE and MSCSci from the University of Minnesota. He was a Principal Systems Engineer at Boston Scientific from 2005 through April 2010. Previously he designed hardware of embedded systems for a large defense contractor, and tried, unsuccessfully, to start a company to build supercomputers using a radically-different architecture. For the supercomputer, he authored a concurrent programming language, and a proof-outline checker to assure total correctness and interference-freedom. BLESS, and its nascent proof tool, build upon this prior work.