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 .
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.
 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).