Kangfeng Ye (also known as Randall Ye)

I am a Research Associate at the University of York, working in the Department of Computer Science.

I am creating a simpler academic homepage and migrating contents from old entry.

My latest CV is available here.

▶︎

all

running...

Short background
- Research Keywords
Research interests and summary
News
- Papers
- Events (I attended)
Awards
Publications
Talks and Presentations
- Probabilistic programming
- Verification of security protocols
Projects (I was or am working on)
Posts
Showcases
Academic activities
Contact

Short background

2016 - now: Academia (Formal methods in robotics, probabilistic programming, and security): In my research, I use mathematical logic (alphabetised predicate calculus in Unifying Theories of Programming - UTP) to give probabilistic semantics (denotational 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 apply theoretical semantics and practical tools to a variety of case studies.; I am a developer of RoboTool supporting probabilistic verification for robotic applications, and a contributor ^[1] of Isabelle/UTP, a unifying semantic framework supporting theorem proving. Both tools are being developed in the RoboStar group.
2012 - 2016: PhD at the University of York (Formal methods): Supervised by Prof. Jim Woodcock. The most right choice in my career is to have a PhD in formal methods with Jim. Every time when I think of him, I always feel 🙂 ☀️ and calm and passionate 🔥 in research because of the knowledge he taught me and the way being a good researcher.; 📚 Thesis: Model Checking of State-Rich Formalisms (By Linking to Combination of State-based Formalism and Process Algebra)
2004 - 2012: Industry (Embedded Software Engineer/Lead): Led a team (4-8 members) to develop embedded software for lithography, Ethernet Datacenter Switch, and Communication devices. C/C++, MCU, Linux, VxWorks

Research Keywords

🔑 Formal verification 🔑 Formal semantics 🔑 Probabilistic programming languages 🔑 Probabilistic model checking 🔑 Probabilistic theorem proving 🔑 Model-based Software Engineering 🔑 Cyber-Physical Systems 🔑 Cryptographic security protocols 🔑 Tool development

Research interests and summary

Probabilistic programming: semantics and verification

➡️ Probabilistic semantics and verification for RoboChart using PRISM

🔆 fully automatic verification of state machines notation using probabilistic model checking
📚: Probabilistic Modelling and Verification Using RoboChart and PRISM
🛠️: Three plugins in RoboTool for 1️⃣ the PRISM metamodel, 2️⃣ RoboChart model transformation to PRISM and verification, and 3️⃣ Probabilistic properties.
📒 RoboChart case studies, High-Voltage Controller (HVC), UV light-treatment (UVC)
- 📚 Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment

➡️ Probabilistic Unifying Relations (ProbURel)

🔆 a probabilistic semantics framework and 🔆 a probabilistic programming language
📚: Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: Semantics and automated reasoning with theorem proving
🛠️: A theory for ProbURel and algebraic laws
📒 Six proved examples including Monty Hall problem, a forgetful Monty, [Doctor Who's Tardis Attacker], robot localisation, cancer diagnosis (Bayesian approach), coin flip till heads, throw a pair of dice till they have the same outcome.

➡️ Probabilistic designs

🔆 a theory for nondeterministic probabilistic sequential programming language
📚: Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving
🛠️: A theory for probabilistic designs in Isabelle/HOL
📒 The proof of an algorithm to get uniform distribution from just a fair coin, and a few other examples from He's and Hehner's PPP papers

➡️ Quantitative Analysis of UML Activity Diagrams

🔆 A UML Profile for Quantitative Annotations 🔆 Semantics of Quantitative Activity Diagrams in PRISM 🔆 Parametric Quantitative Analysis 🔆 Synthesis 🔆 Three Markov models (DTMC, MDP, and CTMC)
📚: Quantitative Assurance and Synthesis of Controllers from Activity Diagrams
🛠️: Eclipse-based Plugins, fully automated, support PRISM and Storm
📒 Seven evaluated examples including Six-sided dice, Digital camera, Fruit picking, Travel web, IT Support, and Travel management from literature. Hospital 🏥 Intralogistics Robot 🤖 by us
- 14 Markov models: 6 in DTMCs, 3 in MDPs, and 5 in CTMCs
🎬 Installation - 1: Eclipse, Papyrus and Epsilon and Installation - 2: Configuration

➡️ QoS (energy efficiency and service availability) analysis of O-RAN xApps

🔆 Compared 6 configurations of control policy for different QoS results
📚: Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification, to appear in DataMod24
🛠️ PRISM models
📒 A scenario with 3 Radio cards + 9 UEs (user equipments) where UEs can be switched on and off based on a continuous distribution (exponential).

Formal specification languages

Z notation and Circus

➡️ Model checking of Circus

🔆 Semantics of Circus in CSP || B 🔆 Automatic transformation of Circus to CSP || B 🔆 Model checking using ProB
📚: Model Checking of State-Rich Formalisms (By Linking to Combination of State-based Formalism and Process Algebra), Model checking of state-rich formalism by linking to $CSP\,\Vert \,B$
🛠️: Circus2CSPZ translator, Java, based on the CZT project
📒 Reactive buffer, Steam boiler, ESEL

➡️ An ISO Z and Circus Parser and Typechecker

🔆 A complete implementation^[2] of ISO Z Standard (ISO/IEC 13568:2002) 🔆 Most Circus Syntax
📚: Haven't published yet 🙁
🛠️: ISOZ and Circus Parser and TypeChecker, implemented using Alex and Happy in Haskell, also C++.
📒 Examples from the standard documentation, Circus buffer, reactive buffer, Circus steam boiler

➡️ Reactive Relations^[3]

🔆 A mechanised theory of Reactive Relations in Isabelle/HOL
📚: Automated verification of reactive and concurrent programs
by calculation
🛠️: The theory of Reactive Relations in UTP
📒 Reactive buffer

CSP

➡️ Animation of RoboChart

🔆 An Interaction-Trees-based deterministic CSP in Isabelle/HOL
📚: Formally verified animation for RoboChart using interaction trees at Journal of Logical and Algebraic Methods in Programming and at ICFEM2022
🛠️: The theory of Interaction Trees based CSP in Isabelle/UTP
📒 Autonomous Chemical Detector, Patrol Robot

Graphical Notations

➡️ Assume-Guarantee Reasoning of Simulink

🔆 A mechanised theory for assume-guarantee reasoning of discrete Simulink in Isabelle/HOL
📚: Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP, Technical report for the mechanised theory
🛠️: The theory of Assume-Guarantee reasoning of Simulink
📒 A post landing finalize subsystem in aircraft cabin pressure control

➡️ Probabilistic semantics and animation for the state-machine based RoboChart (see details above)

➡️ Quantitative Analysis of UML Activity Diagrams (see details above)

Formal verification of security protocols

➡️ Formal verification of security protocols using animation, a lightweight model checker

🔆 An Interaction-Trees-based deterministic CSP used to model security protocols 🔆 Manual + Automatic verification 🔆 User-guided accessible verification 🔆 Terminal + Web interfaces
📚: User-Guided Verification of Security Protocols via Sound Animation
🛠️: A theory of modelling and verifying security protocols in Isabelle/HOL
📒 Needham-Schroeder Public Key Protocol, Diffie-Hellman key agreement

Member of Groups

News

Papers

2025-01-16 Interviewed by Dr. Daniel Shea on Scholarly Communication: I was interviewed on Scholarly Communication by Dr. Daniel Shea from Karlsruhe Institute of Technology (KIT) for one of my co-authored paper: Probabilistic Modelling and Verification Using RoboChart and PRISM. The paper was published in the journal of Software and Systems Modeling and won the Journal-First award. I was invited to present the paper at MODELS 2022.
The episode is now available here.
2024-11-06 The preprint of the DataMod24 paper is available: The preprint of our paper "Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification" can be found here.
2024-10-07 Paper accepted by DataMod24: Our paper submitted to DataMod24 has been accepted for publication. This paper is about the quantitative analysis of a control policy used in an O-RAN xApp to achieve energy efficiency and guarantee service availability. We use PRISM to verify a scenario with 3 radio cells (stations) and 9 UEs (user equipments) while UEs are dynamically and uncertainly switched on and off.
2024-10-01 The preprint of the SEFM2024 paper is available: The preprint of our paper "User-Guided Verification of Security Protocols via Sound Animation" can be found here. Please note that this is not the final camera ready version
2024-09-25: Our TCS journal paper (about probabilistic programming) is now online
2024-09-12: Our TCS journal paper (about probabilistic programming) has been accepted for publication and should be online soon.; The first draft is available online at arxiv
2024-09-01: A joint Festschrift paper, titled "A Tour Through the Programming Choices: Semantics and Applications", with Pedro Ribeiro, Frank Zeyda, and Alvaro Miyazawa to celebrate Prof. Jim Woodcock's retirement from York. He was my PhD supervisor and a line manager in RoboStar.
2024-08-22: Our paper (User-Guided Verification of Security Protocols via Sound Animation) submitted to SEFM24 has been accepted for publication.
2023-12-19: Our JLAMP journal paper (Formally verified animation for RoboChart using interaction trees) has been accepted for publication.

Events (I attended)

2024-11-06 to 2024-11-08: SEFM2024 at Aveiro, Portugal: I presented our work "User-Guided Verification of Security Protocols via Sound Animation" at SEFM2024. The slide is available here
2024-09-26 Cheddar All-hands meeting in Imperial: Presentations from new partners, demonstration discussion, and updates from each pillar. I have updated P3.2 from York regarding accessible formal techniques using sound animation and quantitative analysis of energy efficiency and service availability in O-RAN xApps (to optimise QoS).
2024-09-04 Jim's Festschrift: I have been greatly benefited from Jim’s inspiration and mentorship. I and Pedro presented our paper "A Tour Through the Programming Choices: Semantics and Applications". It's my pleasure to present Frank's preferential choice and my work ProbURel (collaborated with Jim and Simon) in probabilistic semantics and theorem proving.
2024-07-25 6G Summit in Leeds: Co-located with WINCOM2024
2024-07-09: Cheddar project meeting at the Cranfield University
2024-06-27: Gave a talk in the University's Celebrating Spaces: Connecting Researchers. It is a 5-minute Lightning Talk. My talk is about Guarantee correctness and performance of probabilistic algorithms.
2024-06-05 to 06: Cheddar Pillar 1 and P3.2 meetings at the University of Glasgow
2024-03-28: Cheddar P3.1 and P3.2 joint meeting at Imperial College London
2024-03-12: Cheddar Bi-Annual meeting at the University of York

Awards

2022 SoSyM Journal-first: For the paper Probabilistic Modelling and Verification Using RoboChart and PRISM

Publications

Journal article

[ProbURel] K. Ye, J. Woodcock, and S. Foster, “Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: Semantics and automated reasoning with theorem proving,” Theoretical Computer Science, p. 114 876, 2024, issn: 0304-3975. doi: 10.1016/j.tcs.2024.114876.
[RoboChart_ITrees] K. Ye, S. Foster, and J. Woodcock, “Formally verified animation for RoboChart using interaction trees,” Journal of Logical and Algebraic Methods in Programming, vol. 137, p. 100 940, 2024, issn: 2352-2208. doi: 10.1016/j.jlamp.2023.100940.
[RoboChart_PRISM] K. Ye, A. Cavalcanti, S. Foster, A. Miyazawa, and J. Woodcock, “Probabilistic modelling and verification using RoboChart and PRISM,” en, Software and Systems Modeling, vol. 21, no. 2, pp. 667–716, Apr. 2022, issn: 1619-1374. doi: 10.1007/s10270-021-00916-8.
[Reactive_Relations] S. Foster, K. Ye, A. Cavalcanti, and J. Woodcock, “Automated Verification of Reactive and Concurrent Programs by Calculation,” Journal of Logical and Algebraic Methods in Programming, vol. 121, p. 100 681, Jun. 2021, arXiv:2007.13529 [cs], issn: 23522208. doi:
10.1016/j.jlamp.2021.100681.
[ModelChecking_Circus] K. Ye and J. Woodcock, “Model checking of state-rich formalism by linking to $CSP\,\Vert \,B$ ,” en, International Journal on Software Tools for Technology Transfer, vol. 19, no. 1, pp. 73–96, Feb. 2017, issn: 1433-2787. doi: 10.1007/s10009-015-0402-1. (visited on 10/13/2023).

Conference Proceedings

K. Ye, R. Metere, and P. Yadav, “User-Guided Verification of Security Protocols via Sound Animation,” in Software Engineering and Formal Methods (SEFM), Springer Nature Switzerland, Nov. 2024, pp. 33–51, isbn: 9783031773822. doi: 10.1007/978-3-031-77382-2_3.
R. Metere, K. Ye, Y. Gu, et al., “Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification,” in From Data to Models and Back (DataMod2024), Springer International Publishing, 2024.
M. Adam, K. Ye, D. A. Anisi, A. Cavalcanti, J. Woodcock, and R. Morris, “Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment,” in 2023 IEEE 19th International Conference on Automation Science and Engineering (CASE), ISSN: 2161-8089, Aug. 2023, pp. 1–7. 10.1109/CASE56687.2023.10260395.
K. Ye, S. Foster, and J. Woodcock, “Formally Verified Animation for RoboChart Using Interaction Trees,” en, in Formal Methods and Software Engineering, A. Riesco and M. Zhang, Eds., ser. Lecture Notes in Computer Science, Cham: Springer International Publishing, 2022, pp. 404–420, isbn: 978-3-031-17244-1. 10.1007/978-3-031-17244-1_24.
K. Ye, S. Foster, and J. Woodcock, “Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving,” en, in Relational and Algebraic Methods in Computer Science, U. Fahrenberg, M. Gehrke, L. Santocanale, and M. Winter, Eds., ser. Lecture Notes in Computer Science, Cham: Springer International Publishing, 2021, pp. 465–482, isbn: 978-3-030-88701-8. 10.1007/978-3-030-88701-8_28.
J. Woodcock, A. Cavalcanti, S. Foster, A. Mota, and K. Ye, “Probabilistic Semantics for RoboChart,” en, in Unifying Theories of Programming, P. Ribeiro and A. Sampaio, Eds., ser. Lecture Notes in Computer Science, Cham: Springer International Publishing, 2019, pp. 80–105, isbn: 978-3-030-31038-7. 10.1007/978-3-030-31038-7_5.
S. Foster, K. Ye, A. Cavalcanti, and J. Woodcock, “Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra,” en, in Relational and Algebraic Methods in Computer Science, J. Desharnais, W. Guttmann, and S. Joosten, Eds., ser. Lecture Notes in Computer Science, Cham: Springer International Publishing, 2018, pp. 205–224, isbn: 978-3-030-02149-8. 10.1007/978-3-030-02149-8_13.

Books and Chapters

P. Ribeiro, K. Ye, F. Zeyda, and A. Miyazawa, “A tour through the programming choices: Semantics and applications,” in The Application of Formal Methods. Springer Nature Switzerland, 2024, pp. 261–305, isbn: 9783031671142. 10.1007/978-3-031-67114-2_11.
J. Woodcock, S. Foster, A. Mota, and K. Ye, “RoboStar Technology: Modelling Uncertainty in RoboChart Using Probability,” en, in Software Engineering for Robotics, A. Cavalcanti, B. Dongol, R. Hierons, J. Timmis, and J. Woodcock, Eds., Cham: Springer International Publishing, 2021, pp. 413–465, isbn: 978-3-030-66494-7. doi: 10.1007/978-3-030-66494-7_13.
K. Ye, S. Foster, and J. Woodcock, “Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP,” en, in From Astrophysics to Unconventional Computation: Essays Presented to Susan Stepney on the Occasion of her 60th Birthday, ser. Emergence, Complexity and Computation, A. Adamatzky and V. Kendon, Eds., Cham: Springer International Publishing,
2020, pp. 215–254, isbn: 978-3-030-15792-0. doi: 10.1007/978-3-030-15792-0_10.

PhD Thesis

K. Ye, “Model Checking of State-Rich Formalisms (By Linking to Combination of State-based Formalism and Process Algebra),” en, phd, University of York, Aug. 2016. url: https://etheses.whiterose.ac.uk/15526/.

Preprints

K. Ye and J. Woodcock, RoboCertProb: Property Specification for Probabilistic RoboChart Models, 2024. arXiv: 2403.08136 [cs.LO].
K. Ye, F. Yan, and S. Gerasimou, Quantitative Assurance and Synthesis of Controllers from Activity Diagrams, 2024. arXiv: 2403.00169 [cs.LO].

Talks and Presentations

Probabilistic programming

Lightning Talk on 2024-06-27: A 5-minute Lightning Talk, given at the University's Celebrating Spaces: Connecting Researchers. The talk video is now available at Youtube. My talk is about Guarantee correctness and performance of probabilistic algorithms.

Verification of security protocols

Presentation at SEFM2024 on the 7th of November, 2024: I presented our paper "User-Guided Verification of Security Protocols via Sound Animation" at SEFM2024. In this work, we address the accessibility of formal verification of security protocols for designers and the soundness guarantee of automatically generated animators. The slide is available here. More details can be found this post.

Projects (I was or am working on)

CHEDDAR (Feb 2024 - ): The Communications Hub for Empowering Distributed Cloud Computing Applications and Research (CHEDDAR)
SESAME (June 2023 - Jan 2024): Secure and Safe Multi-Robot Systems
RoboCalc and RoboTest (April 2018 - June 2023): EPSRC projects in the RoboStar group
CyphyAssure (June 2021 - September 2021): A EPSRC-funded (Simon Foster's fellowship) project
Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP (Oct 2017 - March 2018): A VETSS sponsored project
INTO-CPS (Nov 2016 - Dec 2017): Integrated Tool Chain for Model-based Design of Cyber-Physical Systems

Posts

2024-11-06 to 08: Application of formal verification in security protocols and O-RAN xApps

Showcases

Academic activities

Organiser of WINCOM2024 Hackathon and Demo: Organised with Ashan Khan together
JWFS 2024 PC member: The Festschrift for Prof. Jim Woodcock on the occasion of his retirement from the University of York

Contact

I made a few contributions to Isabelle/UTP, particularly in reactive designs and interaction trees. But in general, I am a user of Isabelle/UTP, and not a developer. ↩︎
Except semantics transformation rules (a small part is implemented) ↩︎
relatively small contribution to this work, mainly in the verificaiton of the reactive buffer, and gave Simon some insight on the verificaiton strategy when he was developing the theory. But this is very beautiful work and it is nice to mention here. ↩︎
Circus members are now mostly in RoboStar ↩︎