Compositional Verification of Architectural Models

Presented as part of the 2012 HCSS conference.

Abstract:

This talk presents a design flow and supporting tools to significantly improve the design and verification of complex cyber-physical systems.  We focus on system architecture models composed from libraries of components and complexity-reducing design patterns having formally verified properties. This allows new system designs to be developed rapidly using patterns that have been shown to reduce unnecessary complexity and coupling between components. Components and patterns are annotated with formal contracts describing their guaranteed behaviors and the contextual assumptions that must be satisfied for their correct operation.  We describe a compositional reasoning framework for proving the correctness of a system design, and present an example based on an aircraft flight control system to illustrate the method and supporting analysis tools.

Biography:

Darren Cofer is a Principal Systems Engineer in the Trusted Systems group of ATC. He earned his PhD in Electrical and Computer Engineering from The University of Texas at Austin. His principal area of expertise is developing and applying advanced analysis methods and tools for verification and certification of high-integrity systems. His background includes work with formal methods for system and software analysis, the design of real-time embedded systems for safety-critical applications, and the development of nuclear propulsion systems in the U.S. Navy. He is currently the principal investigator on Rockwell Collins’ META project with DARPA, and serves on RTCA committee SC-205 tasked with developing DO-178C, providing updated certification guidance for airborne software. He is an Associate Technical Editor for Control Systems Magazine and is a Senior Member of the IEEE.