formal methods

file

Visible to the public Formal Models of Human Control and Interaction with Cyber Physical Systems.pdf

Submitted by Katia Sycara on Mon, 12/22/2014 - 11:55am. Contributors:

Abstract:

One of the most important challenges in the design and deployment of Cyber-Physical Systems is how to formally guarantee that they are amenable to effective human control. This is a challenging problem not only because of the operational changes and increasing complexity of future CPS but also because of the nonlinear nature of the human-CPS system under realistic assumptions.

file

Visible to the public Development of Novel Architectures for Control and Diagnosis of Safety-Critical Complex Cyber-Physical Systems

Submitted by necozay on Mon, 11/10/2014 - 1:49pm. Contributors:

Abstract:

The project is developing novel architectures for control and diagnosis of complex cyber--physical systems subject to stringent performance requirements in terms of safety, resilience, and adaptivity. These ever--increasing demands necessitate the use of formal model--based approaches to synthesize provably--correct feedback controllers.

file

Visible to the public Credible Autocoding and Verification of Embedded Software (CrAVES)

Submitted by rjobredeaux3 on Mon, 11/10/2014 - 1:49pm. Contributors:

Abstract:

The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which graphical control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems.

file

Visible to the public Efficient Traffic Management: A Formal Methods Approach

Submitted by arcak on Mon, 11/10/2014 - 1:49pm. Contributors:

Abstract:

The objective of this project is to develop a formal methods approach to traffic management. Formal methods is an area of computer science that develops efficient techniques for proving the correct operation of systems, such as computer programs and digital circuits, and for designing systems that are correct by construction.