High-level property specification languages

One of the key aspects in formal verification is to precisely formalize the requirements of a system. Typically, we do this using temporal logics such as LTL, CTL, CTL* or the modal mu-calculus. However, using these languages requires a lot of expertise.

To make the formal specification of requirements easier, people have been investigating languages and methods that require less expertise. One particularly well-known approach are property specification patterns [1].

In this project, you perform a literature review, for instance using snowballing, to create on overview of high-level approaches to property specification, and make a comparison of these approaches.

[1] Dwyer, M.B. et al.: Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002). pp. 411-420 (1999).