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.

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.

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.

Abstract: Optimization algorithms used in a real-time and safety-critical context offer the potential for considerably advancing robotic and autonomous systems by improving their ability to execute complex missions. However, this promise cannot happen without proper attention to the considerably stronger operational constraints that real time, safety-critical applications must meet, unlike their non-real-time, desktop counterparts.

Abstract: As part of our CPS project, we have focused on the problem of model repair for cyber-physical systems. This work involves identifying constraints caused due to physical components during revision. We consider four types of constraints cyber-cyber, cyber-physical, physical-cyber and  physical-physical. Based on the complexity limitations caused by these constraints we are developing efficient heuristics to mitigate the cost of model repair. We have also focused on extending revision to code level.