Visualisation of TLA+ specifications

Primary supervisor

Humphrey Obie

Mission-critical systems have to comply to various formal standards – e.g. DO-178C and ISO26262 - about their operation, usually heavily relying on formal specification languages such as TLA+. This presents many challenges to developers in terms of how to write, read and communicate the target system’s formal specifications. In most cases, having the right formal methods experts to write specifications does not solve the problem as the wider development team needs to be able to deeply understand the formal specifications. This project will explore visualisation techniques to translate systems’ specifications developed in TLA+ into user-friendly diagrams/visualisations that are easy to understand.
 

Student cohort

Single Semester
Double Semester

URLs/references

  • S. Resch and M. Paulitsch, "Using TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware," IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), Toulouse, pp. 146-152, IEEE, 2017.
  • L. Lamport, "The PlusCal algorithm language." In International Colloquium on Theoretical Aspects of Computing, pp. 36-60. Springer, Berlin, Heidelberg, 2009.

  • Harel, David. "On visual formalisms." Communications of the ACM 31.5 (1988): 514-530.


     

Required knowledge

  • Good understanding of model-driven engineering
  • Programming experience (preferably Java)
  • Knowledge of discrete mathematics and logic
  • Knowledge of information visualisation