It is well understood that many cyber-physical systems incorporate software that is getting increasingly complex, hard to manage, and therefore often quite fragile. We will present our recent work on addressing this challenge using formal methods based tools and techniques for creation of software for cyber-physical systems that provide strong assurances that the resulting software would be secure, safe, and reliable.

These include - the use of a formally verified operating system; - the use of a toolchain where proofs of controller safety properties in a theorem prover for hybrid systems are used for synthesis of high assurance high performance control code implementations; - leveraging general-purpose formal tools to create automated synthesizers for high assurance message handling code that comes with proofs of correctness (which imply absence of misbehaviors due to e.g. malformed messages); and - tools for producing high assurance and medium assurance glue code that links different modules in a secure safe and resilient manner.

This talk will primarily present a tool user perspective – outlining how we applied these tools and describing both successes and challenges of this effort.