Visible to the public CPS Architectures

The mission of this online community of CPS architectures is to share research results on using cyber-physical system architectures to support design, analysis and verification of complex cyber-physical systems using heterogeneous modeling formalisms.


Visible to the public Adaptive Cruise Control-Hybrid Distributed and Now Formally Verified

Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified


Visible to the public Using Theorem Provers to Guarantee Closed-Loop System Properties

Abstract--This paper presents a new approach for leveraging the power of theorem provers for formal verification to provide sufficient conditions that can be checked on embedded control designs. Theorem provers are often most ecient when using generic models that abstract away many of the controller details, but with these abstract models very general conditions can be verified under which desirable properties such as safety can be guaranteed for the closed-loop system. We propose