Cyber Physical Systems (CPS) interact with their surroundings and may, through malfunction or design oversights, cause or allow harm to people, property, the environment, or national security. Certification is the process for providing assurance that deploying a given system does not pose an unacceptable risk of adverse consequences. Current certification methods, which largely rely on recommended practices, extensive documentation, and human review, are costly and burdensome, worryingly fallible, and a barrier to innovation.
This research is advancing emerging new certification practices based on explicit goal based assurance cases. It is developing the scientific foundations of certification based on multi-legged arguments in which some of the legs can be generated automatically using advanced formal methods. Furthermore, the research is developing methods by which certification can be performed compositionally, allowing the development of certified components and easing the certification of systems based on these.
Certification requires anticipation, at the time of design and review, of all the circumstances that a system will encounter in its lifetime. Future cyber physical system will configure or even assemble themselves dynamically, so the research is developing methods by which some of the anticipation of future circumstances can be performed at runtime, and harmful outcomes avoided by runtime adaptation. Much of the assurance required for certification is thereby moved to runtime, yielding "just-in-time certification." The technical foundations for these methods lie in automated abstractions of hybrid systems, controller synthesis, and mechanizations of these based on high performance SMT solvers.
The project engages with certification bodies so that its research results can inform future certification practices.
