Formal verification

CHEDDAR (Feb 2024 - )
The Communications Hub for Empowering Distributed Cloud Computing Applications and Research (CHEDDAR)
The submission (Formally Verified Animation for RoboChart using Interaction Trees) to ICFEM2022 is accepted
Jun 27, 2022
CyPhyAssure (June 2021 - August 2021)
CyPhyAssure is a EPSRC funded project. It is also a RoboStar project.
CyPhyAssure (June 2021 - August 2021)
RoboTest (April 2021 - Present)
RoboTest is a EPSRC funded project. It is also a RoboStar project.
RoboTest (April 2021 - Present)
Modelling and verification of probabilistic behaviour of robotic applications
This talk presents how our RoboTool uses PRISM to analyse probability properties of robotic applications by transforming RoboChart to PRISM.
Jul 23, 2019
Project
Modelling and verification of probabilistic behaviour of robotic applications
RoboCalc (April 2018 - March 2021)
RoboCalc is a EPSRC funded project. It is also a RoboStar project.
RoboCalc (April 2018 - March 2021)
VeTSS - Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP (Oct 2017 - March 2018)
A UK National Cyber Security Centre (NCSC) funded project and we have developed a theoretical reasoning framework for discrete-time blocks of control law diagrams.
VeTSS - Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP (Oct 2017 - March 2018)
INTO-CPS (Dec 2016 - Dec 2017)
INTO-CPS (Integrated Tool Chain for Model-based Design of Cyber-Physical Systems) is a EU Horizon 2020 project, from 2015 to 2017. Please see http://into-cps.org/about-the-project/ for more information about this project.
INTO-CPS (Dec 2016 - Dec 2017)
Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP
This report is a summary of our work for the VeTSS funded project ?Mechanised Assume-Guarantee Reasoning for Control Law Diagrams via …
<ins>Kangfeng Ye</ins>, Simon David Foster, JAMES Charles Paul Woodcock
PDF