Kangfeng (Randall) Ye

Kangfeng (Randall) Ye

Research Associate (Computer Science)

University of York

Biography

I am a research associate at the University of York and working on formal verification of robotics and cyber-physical systems using model checking and theorem proving. I am particularly interested in applying mathematics, logic, and model-based techniques to ensure dependability as computer systems, especially safety-critical systems, are becoming increasingly complex. In my research, I (1) use mathematical logic (alphabetised predicate calculus in Unifying Theories of Programming - UTP) to give (probabilistic) semantics (denotational semantics and operational semantics) to a domain-specific language (RoboChart) in robotics, with support of modelling time and probability, (2) develop automated verification tools using modern model-based techniques (model transformation, validation, and generation) and formal verification (model checking and theorem proving), and (3) apply theoretical semantics and practical tools to a variety of case studies. I am a developer of RoboTool and Isabelle/UTP, the tools developed in our RoboStar group to support modelling and automated verification.

My recent work is summarised in two posters (probabilistic modelling and verification in RoboChart and Formally Verified Animation of RoboChart using interaction trees) and demonstrated (Automated probabilistic verification of RoboChart using PRISM, Animation of the autonomous chemical detector RoboChart model, and Animation of a patrol robot model).

Before I moved to academia in 2012 to pursue a PhD, I have eight years of experience as a senior software and firmware leader in industry: R&D in semiconductor equipment and high-end ToR data centre switches. I have seen some major challenges that traditional software and system engineering is facing: for example, dependability and assurance are not guaranteed. This motivated my interest in formal methods.

Download my CV .

Interests
  • Uncertainty modelling
  • Probabilistic modelling
  • Probabilistic verification
  • Probabilistic programming languages
  • Statistics inference
  • Denotational and operational semantics
  • Formal verification (model checking and theorem proving)
  • Model-based techniques
  • Robotics and CPS
Education
  • PhD in Computer Science, 2016

    University of York

Recent Posts

Probabilistic vs. Stochastic
In our paper “Probabilistic modelling and verification using RoboChart and PRISM”, a statement “NFM-1 is needed due to the fact that DTMCs and MDPs are stochastic. Any state in a PRISM model has to have at least one outgoing transition.” is not fully explained. I am going to explain here.

Projects

*
SESAME (June 2023 - Dec 2023)
SESAME: Secure and Safe Multi-Robot Systems is a Horizon2020 project. It is a project associated with the Automated Software Engineering (ASE) group.
SESAME (June 2023 - Dec 2023)
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)
RoboCalc (April 2018 - March 2021)
RoboCalc is a EPSRC funded project. It is also a RoboStar project.
RoboCalc (April 2018 - March 2021)
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)

Recent Publications

Quickly discover relevant content by filtering publications.
(2023). Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment. 2023 IEEE 19th International Conference on Automation Science and Engineering (CASE).

Cite DOI

(2022). Formally Verified Animation for RoboChart Using Interaction Trees. Formal Methods and Software Engineering.

PDF Cite DOI

(2021). Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving. Relational and Algebraic Methods in Computer Science.

PDF Cite DOI

(2021). Probabilistic modelling and verification using RoboChart and PRISM. Software and Systems Modeling.

PDF DOI

(2021). Automated verification of reactive and concurrent programs by calculation. Journal of Logical and Algebraic Methods in Programming.

PDF Cite DOI

(2021). RoboStar Technology: Modelling Uncertainty in RoboChart Using Probability. Software Engineering for Robotics.

PDF Cite DOI

(2020). Automated Verification of Reactive and Concurrent Programs by Calculation. CoRR.

PDF

(2020). Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP. From Astrophysics to Unconventional Computation: Essays Presented to Susan Stepney on the Occasion of her 60th Birthday.

PDF DOI

(2019). Probabilistic Semantics for RoboChart - A Weakest Completion Approach. Unifying Theories of Programming - 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings.

PDF DOI

(2018). Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP.

PDF

(2018). Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. CoRR.

PDF

(2018). Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. Relational and Algebraic Methods in Computer Science.

PDF DOI

(2017). Model checking of state-rich formalism by linking to $$CSP,‖ ,B$$CSP‖B. International Journal on Software Tools for Technology Transfer.

PDF DOI

Contact Me