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
 |
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
|
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
 |
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.
|
SMACCM
 |
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
