Research Interests
I am interested in the application to the formal verification of properties
of concurrent systems, and have been working for a couple of years on
modelling and verifying liveness properties of security protocols. For
example, we have proved the correctness of the fairness property of the
Zhou-Gollmann Non-repudiation Protocol by embedding the denotational
semantics of the stable failures model of CSP in the PVS theorem prover. I
am also interested in the
Unifying Theories of Programming (UTP)
that is based on the alphabetised relational calculus.
I have recently involved in the
INDEED project whose aim is to develop
knowledge, methods and tools that contribute to the understanding of
socio-technical system dependability, and that support developers of
dependable systems. In York's workpackage, we take advantage of the
timebands model to handle complex systems. To formalise the timebands model,
we are extending the
Circus language to a timed model. We have also
combined the miracle, the top element of a complete lattice, in the timed
Circus to specify those brand-news features of the timebands model.
Publications
[WWB11b] Kun Wei, Jim Woodcock and Alan Burns, Modelling Temporal Behaviour
in Complex Systems with Timebands, a chapter to a Springer book (to appear
soon).
[WWB11a] Kun Wei, Jim Woodcock and Alan Burns, Timed Circus: Timed CSP with
the Miracle. Accepted by ICECCS2011.
[WWB10c] Kun Wei, Jim Woodcock and Alan Burns, Embedding the timed Circus in
PVS. Technical Report, University of York. [
pdf]
[WWB10b] Kun Wei, Jim Woodcock and Alan Burns, Formalising the Timebands
Model in Timed Circus. Technical Report. University of York. [
pdf]
[WWB10a] Kun Wei, Jim Woodcock, Alan Burns, "A Timed Model of Circus with
the Reactive Design Miracle," SEFM, pp.315-319, 2010 8th IEEE International
Conference on Software Engineering and Formal Methods, 2010.
[JMAK10] Jim Woodcock, Marcel Oliveiray, Alan Burns and Kun Wei, Modelling
and Implementing Complex Systems with Timebands, SSIRI 2010, Singapore.
[W06] Kun Wei, Analysis of Liveness Through Proofs. The PhD thesis. [
pdf]
[WH06b] James Heather and Kun Wei, Where Next for Formal Methods? Security
Protocols Workshop 2006:52-58
[WH06a] Kun Wei and
James Heather, A Theorem-Proving Approach to Verification of Fair
Non-repudiation Protocols.
Formal Aspects in Security and Trust 2006: 202-219. [
pdf]
[WH05b] Kun Wei and
James Heather, Towards Verification of Timed Non-repudiation Protocols.
Formal Aspects in Security and Trust 2005: 244-257. [
pdf]
[WH05a] Kun Wei and
James Heather: Embedding the Stable Failures Model of CSP in PVS.
IFM 2005: 246-265.[
pdf]
