University of Minnesota


Current Projects

The Critical Research Group has over the years been involved in a multitude of projects. Most of the projects have centered around formal modeling of software and system specification, and the various development activities enabled if such formal specifications are available.

  • CPS:Large: Assuring the Safety, Security and Reliability of Medical Device Cyber Physical Systems

    nsf Medical device systems are a prime example of cyber-physical systems, featuring complex and close interaction of sophisticated treatment algorithms with the physical aspects of the system, and especially the patient whose safety is of the utmost concern. As such systems become increasingly complex, interconnected, and interoperating, the major challenge is how to ensure and improve the safety, security, and reliability of medical device cyber-physical systems. Novel design methods and certification techniques will significantly improve patient safety. This project is aimed at identifying and demonstrating innovative and effective development techniques and certification aids that would help improving the patient safety

  • CPS: Medium :Embedded Fault Detection for Low-Cost, Safety-Critical Systems

    nsf Fault tolerance is vital to ensuring the integrity and availability of safety critical systems. Current solutions are based almost exclusively on physical redundancy at all levels of the design. A fault tolerant system must include the logic and algorithms for fault detection, fault diagnosis, fault containment, and reconfiguration to continue operation in face of failures. Our main research focus will be on one specific—but imperative—sub-problem: the development of algorithms and computing architectures which enable the detection of faults without relying on physical redundancy. In this context, we aim to address both detection of faults in the physical domain (sensor, actuator, and environment faults) as well as faults in the logical—cyber—domain (software and processor faults).

  • Guardol

    DOD Guardol is a domain-specific language focused on the creation of high-assurance network guards and the specification of guard properties. The Guardol system generates Ada code from Guardol programs and also provides specification and automated verification support. Guard programs and specifications are translated to higher order logic, then deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data. The result is that di cult properties of Guardol programs can be proved fully automatically.


    rockwell New generations of military vehicles, including unmanned air vehicles (UAVs), are almost universally being equipped with network interfaces. In addition to the baseline control and monitoring capabilities, network connectivity can provide advanced features such as the ability to adapt to new missions through field upgrades and remote access for maintenance. These network connections typically rely on standard protocols for compatibility with other networked systems and reduction of cost through the use of COTS equipment. As UAV systems continue this rapid evolution toward network access, there is great danger that insufficient attention is being paid to security concerns. A new approach based on comprehensive use of formal methods throughout the development process is needed to ensure that such vulnerabilities are eliminated from critical military assets. Rockwell Collins and University of Minnesota teams bring together key technologies and leading researchers with the experience needed to create a revolutionary approach to the development of these high-assurance systems.

    View Past projects

    • Website design by Gregory Gay and Anitha Murugesan.
    • © 2015 Regents of the University of Minnesota. All rights reserved.
    • The University of Minnesota is an equal opportunity educator and employer. Privacy
    • Last modified on October 30, 2015