Swansea Railway Verification Group
Journal Publications
- 1
- Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, and Helen Treharne.
On modelling and verifying railway interlockings: tracking train lengths.
Science of Computer Programming, 96:315–336, 2014. PDF
- 2
- Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, and Helen Treharne.
Techniques for modelling and verifying railway interlockings.
International Journal of Software Tools for Technology Transfer, 16:685–711, 2014. PDF
- 3
- Phillip James and Markus Roggenbach.
Encapsulating formal methods within domain specific languages: A solution for verifying railway scheme plans.
Mathematics in Computer Science, 8:11–38, 2014. PDF
- 4
- Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, and Helen Treharne.
Railway modelling in CSP||B: the double junction case study.
Electronic Communications of the EASST, 2012. PDF
- 5
- Phillip James and Markus Roggenbach.
Automatically verifying railway interlockings using SAT-based model checking.
Electronic Communications of the EASST, 2010. PDF
- 6
- Karim Kanso, Faron Moller, and Anton Setzer.
Automated verification of signalling principles in railway interlockings.
Electronic Notes in Theoretical Computer Science, 250:19–31, 2009. PDF
Conferences
- 1
- Phillip James, Karim Kanso, Andrew Lawrence, Faron Moller, Markus Roggenbach, Monika Seisenberger, Anton Setzer, and Simon Chadwick.
Verification of solid state interlocking programs.
In Proceedings of SEFM'13, LNCS 8368, 253–268. Springer, 2014. PDF
- 2
- Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, Helen Treharne, Matthew Trumble, and David Williams.
Verification of scheme plans using CSP||B.
In Proceedings of SEFM'13, LNCS 8368, 189–204. Springer, 2014. PDF
- 3
- Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, and Helen Treharne.
Towards the verification of bidirectional railway models in CSP||B.
In Pre-Proceedings of AVoCS'14, 239–241. 2014. PDF
- 4
- Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, and Helen Treharne.
Decomposing scheme plans to manage verification complexity.
In Proceedings of FORMS/FORMAT 2014. 2014. PDF
- 5
- Lloyd Roberts, Mike Smith, Faron Moller, and and Markus Roggenbach.
Visualising timed CSP train simulations for capacity.
In Proceedings of CGVC 2014, 91–93. 2014. PDF
- 6
- Phillip James, Matthew Trumble, Helen Treharne, Markus Roggenbach, and Steve Schneider.
OnTrack: An open tooling environment for railway verification.
In Proceedings of NASA Formal Methods'13, LNCS 7871, 435–440. 2013. PDF
- 7
- Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, and Helen Treharne.
Defining and model checking abstractions of complex railway models using CSP||B.
In Proceedings of HVC'12, LNCS 7857, 193–208. 2013. PDF
- 8
- Phillip James, Arnold Beckmann, and Markus Roggenbach.
Using domain specific languages to support verification in the railway domain.
In Proceedings of HVC'12, LNCS 7857, 274–275. 2013. PDF
- 9
- Yoshinao Isobe, Faron Moller, Hoang Nga Nguyen, and Markus Roggenbach.
Safety and line capacity in railways.
In Proceedings of iFM'12, LNCS 7321, 54–68. Springer, 2012. PDF
- 10
- Marc Fontaine, Andy Gimblett, Faron Moller, Hoang Nga Nguyen, and Markus Roggenbach.
Timed CSP simulator.
In Proceedings of iFM'12 Posters & Tool Demos Session, 41–45. 2012. PDF
- 11
- Yoshinao Isobe, Faron Moller, Hoang Nga Nguyen, and Markus Roggenbach.
Using CSP||B and ProB for railway modelling.
In Proceedings of iFM'12 Posters & Tool Demos Session, 31–35. 2012. PDF
- 12
- Phillip James, Alexander Knapp, Till Mossakowski, and Markus Roggenbach.
Designing domain specific languages - A craftsman's approach for the railway domain using CASL.
In Proceedings of WADT'12, LNCS 7841, 178–194. 2012. PDF
- 13
- Phillip James and Markus Roggenbach.
Designing domain specific languages for verification - first steps.
In Proceedings of ATE'11, 40–45. 2011. PDF
Abstracts
- 1
- Phillip James.
Verification of train control systems: Reducing the complexity.
In BCTCS'10: The 26th British Colloquium for Theoretical Computer Science, University of Edinburgh. April 2010. PDF
- 2
- Karim Kanso.
Model checking from a type theory platform.
In BCTCS'10: The 26th British Colloquium for Theoretical Computer Science, University of Edinburgh. April 2010. PDF
- 3
- Andrew Lawrence.
Verifying railway interlockings using SCADE.
In BCTCS'10: The 26th British Colloquium for Theoretical Computer Science, University of Edinburgh. April 2010. PDF
- 4
- Phillip James.
Verifying train control systems - using SAT-based model checking.
In BCTCS'09: The 25th British Colloquium for Theoretical Computer Science, University of Warwick. April 2009. PDF
- 5
- Karim Kanso.
Automated generation of verified railway interlocking systems.
In BCTCS'09: The 25th British Colloquium for Theoretical Computer Science, University of Warwick. April 2009. PDF
- 6
- Phillip James and Markus Roggenbach.
SAT-based model checking of train control systems.
In CALCO-jnr'09: The CALCO Young Researchers Workshop, University of Udine. September 2009. PDF
- 7
- Karim Kanso.
Formal verification of safety properties in systems defined in Ladder Logic.
In BCTCS'08: The 24th British Colloquium for Theoretical Computer Science, Durham University. April 2008. PDF
Theses
- 1
- Karim Kanso.
Agda as a Platform for the Development of Verified Railway Interlocking Systems.
PhD thesis, Swansea University, 2012. PDF
- 2
- Andrew Lawrence.
Verification of Railway Interlockings in SCADE.
Master's thesis, Swansea University, 2011. PDF
- 3
- Phillip James.
SAT-based Model Checking and its Applications to Train Control Software.
Master's thesis, Swansea University, 2010. PDF
- 4
- Karim Kanso.
Formal Verification of Ladder Logic.
Master's thesis, Swansea University, 2008. PDF
- 5
- Andy Ryan.
Formal Specification of Moving Block Railway Interlocking Using CASL.
BSc Dissertation, 2010. PDF