Papers

file

Visible to the public Distributed Theorem Proving for Distributed Hybrid Systems.pdf

Submitted by sloos@cs.cmu.edu on Mon, 10/01/2012 - 12:34pm

Title
Distributed Theorem Proving for Distributed Hybrid Systems

file

Visible to the public Towards Formal Verification of Freeway Traffic Control

Submitted by sloos@cs.cmu.edu on Mon, 10/01/2012 - 12:33pm

Title
Towards Formal Verification of Freeway Traffic Control

file

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

Submitted by arajhans on Mon, 08/06/2012 - 3:41pm

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

file

Visible to the public Using Parameters in Architectural Views to Support Heterogeneous Design and Verification Akshay

Submitted by arajhans on Fri, 08/03/2012 - 3:47pm

Abstract--Current methods for designing cyber-physical systems lack a unifying framework due to the heterogeneous nature of the constituent models and their respective analysis and verification tools. There is a need for a formal representation of the relationships between the different models. Our approach is to

file

Visible to the public View Consistency in Architectures for Cyber-Physical Systems

Submitted by arajhans on Wed, 08/10/2011 - 4:23pm

Abstract:

Current methods for modeling, analysis, and design of cyber-physical systems lack a unifying framework due to the complexity and heterogeneity of the constituent elements and their interactions. Our approach is to define relationships between system models at the architectural level, which captures the structural interdependencies and some semantic interdependencies between representations without attempting to comprehend all of the details of any particular modeling formalism.