View Proposal

---

Proposer

Hind Zantout

Title

An Accessible Formal Verification Tool: Bridging Behaviour-Level Modelling and TLA+ Formal Verification System to Improve Usability, Accessibility and Adoption of Formal Verification Technique

Goal

Bridging Behaviour-Level Modelling and TLA+ Formal Verification System to Improve Usability, Accessibility and Adoption of Formal Verification Techniques

Description

The proposed system is based on TLA+ which is an open-source formal specification and model checking tool and PlusCal which is a high-level algorithmic language that helps systems to be translated into formal TLA+. • TLA+ and its model checker (TLC) are available for free and intended for research as well as academic use making them suitable for this project. Many tutorials and online communities exist based on study of the same. • The proposed system will allow a behaviour-level model to PlusCal to TLA+ translator that enables formal verification without requiring users to understand the semantics of TLA+ and its syntax. • The translator aims to be implemented as a deterministic compilation that converts user-created input into a formally verifiable specification in TLA+. Rather than making the input entirely informal, the system will constrain the input to behaviourally meaningful elements while also keeping them easy to understand and interpret from a developer’s perspective. These elements will allow a precise mapping into PlusCal algorithms which make it easier to translate into TLA+ specifications.

Resources

Background

Url

Difficulty Level

Moderate

Ethical Approval

None

Number Of Students

1

Supervisor

Hind Zantout

Keywords

Degrees

Master of Science in Software Engineering