Visible to the public CPS: Medium: GOALI: An Architecture Approach to Heterogeneous Verfication of Cyber-Physical Systems

Project Details
Lead PI:Bruce Krogh
Co-PI(s):David Garlan
Andre Platzer
Prashant Ramachandra
Performance Period:09/15/10 - 08/31/15
Institution(s):Carnegie-Mellon University
Sponsor(s):National Science Foundation
Award Number:1035800
2222 Reads. Placed 20 out of 803 NSF CPS Projects based on total reads on all related artifacts.
Abstract: The objective of this research is to develop new methods for verifying the safety of complex cyber-physical systems based on information derived from the wide variety of models and methods used throughout the design process. The approach is based on a new formalism to represent the architecture of systems with cyber components, physical components, and interconnections between these domains. Diverse engineering models of different aspects of the system will be associated through the cyber-physical architecture for the complete system. Formal logic will be developed to express and reason about inter-model consistency and to infer system-level properties from information derived from the domain-specific models. The project's intellectual merit lies in the creation of a comprehensive, unified framework for verifying properties of systems rich in both cyber and physical components. The new formal logic will make it possible to integrate information from the wide range of engineering domains and technical expertise required to design complex systems. This will lead to a principled, rigorous approach to system-level verification engineering for real-world cyber-physical systems. The application of the new methodology to verify the safety of cooperative intersection collision avoidance systems will have immediate impact on emerging technologies for safer automobile systems. A new interdisciplinary course in engineering and computer science on system-level design of cyber-physical systems will prepare a new cadre of graduates with the cross-cutting skills needed to develop safety-critical systems. Innovative educational modules will also be developed to inspire pre-college students to pursue education and careers in engineering and computer science.
AttachmentTaxonomyKindSize
The KeYmaera X Theorem Prover for Hybrid SystemsPDF document258.84 KBDownloadPreview
Forward Invariant Cuts to Simplify Proofs of SafetyPowerPoint presentation904.58 KBDownloadPreview
An Architectural Approach to Heterogeneous Modeling and Verification of CPSPowerPoint presentation964.76 KBDownloadPreview
Heterogeneous Verification of CPS Using Behavior SemanticsPowerPoint presentation1.09 MBDownloadPreview
GOALI: An Architecture Approach to Heterogeneous Verification of Cyber-Physical SystemsPDF document11.34 KBDownloadPreview
An Architecture Approach to Heterogeneous Verification of CPSPDF document2.69 MBDownloadPreview