Rockwell Collins

file

Visible to the public Automated Deductive Translation of Guardol Programs and Specifications into SMT-Provable Properties

The verification architecture of the Guardol system uses an implementation of HOL (Higher Order Logic) as a front end to SMT (Satisfiability Modulo Theories) technology. SMT provides high levels of proof automation. HOL provides semantic power, modelling the operational semantics of Guardol, an imperative language, and justifying the automatic deductive translation of programs to the functional form needed by SMT technology. In the Guardol system, extensive manipulation of programs and specifications is performed in HOL before goals are sent to the backend RADA SMT system.

file

Visible to the public Lessons from Twenty Years of Industrial Formal Methods

Abstract:

Over the last two decades formal methods have achieved widespread use by industry in the development of safety and security critical systems. However, these successes often go unacknowledged as evidence of the successful transition of formal methods simply because

file

Visible to the public Compositional Verification of Architectural Models

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.

file

Visible to the public Compositional Verification of Architectural Models

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.