Mathematical theories and formal techniques for compositional verification, operational requirements, and uncertainty quantification (UoY lead)
Provide justification based on mathematical theories for the correctness of RoboSAPIENS techniques. Develop new unified theories for data, reaction, time, and uncertainty. Develop prototype tools that support the application of these theories. Supports objectives O1 and O4.
Lead: University of York (UoY) · Effort: 81 person-months · Duration: M1–M36
T1.1: Compositional Verification (M1–M36) — Formal modelling using architectural notation with process algebra semantics, enabling compositional verification of self-adaptive robotic systems.
T1.2: Capturing and Using Operational Requirements in Verification (M1–M36) — Domain-specific notation and controlled natural language for capturing operational requirements and integrating them into the verification process.
T1.3: Uncertainty Quantification (M1–M36) — Metrics for deep learning models, application of the Cynefin framework, and development of a classification algorithm for uncertainty quantification.
T1.4: Prototype Verification Tools (M1–M36) — Tools for architectural modelling and compositional verification, supporting the practical application of the formal theories developed in T1.1–T1.3.
Formal theories, prototype verification tools, technical reports, and scientific publications.
AU, UA, SRL, UoY (lead)