PRISMATIC: Unified Hierarchical Probabilistic Verification Tool
PRISMATIC is a 1 year project being undertaken jointly with
US R&D company SIFT
and Carnegie Mellon University (CMU).
At Oxford, The project is led by
Marta Kwiatkowska
and Dave Parker.
The PRISMATIC project will focus on probabilistic verification of system designs.
It aims to develop a workflow/process and tool to generate probabilistic
"certificates of correctness" for cyber-physical systems, and will be based on
probabilistic and statistical model checking, and in particular the
PRISM model checker.
The project is funded under DARPA's
META program.
From the DARPA website:
"The ultimate goal of the META program is to make a dramatic improvement on the existing systems engineering, integration, and testing process for defense systems... it aims to develop model-based design methods for cyber-physical systems far more complex and heterogeneous than those to which such methods are applied today; to combine these methods with a rigorous deployment of hierarchical abstractions throughout the system architecture; to optimize system design with respect to an observable, quantitative measure of complexity for the entire cyber-physical systems; and to apply probabilistic formal methods to the system verification problem, thereby dramatically reducing the need for expensive real-world testing and design iteration."
People (at Oxford):
More information:
