Model checking requirements specifications: a retrospective

Abstract

Formal methods applied to requirements specification can be categorized into model-based and property-based approaches, each with distinct advantages in formalizing and verifying different aspects of system requirements. This paper provides a retrospective review of Formal Tropos, a pioneering methodology in Requirements Engineering (RE). The groundbreaking idea of Formal Tropos is the coupling of early requirements specifications with formal verification techniques, notably model checking, to enable rigorous, scalable validation. We trace its evolution from its inception to its extensions into goal reasoning using SAT/SMT solvers and its conceptual parallels in the domain of smart legal contracts. A literature review is presented to demonstrate the widespread impact of Formal Tropos on academic research and its application in industrial case studies. We conclude with a forward-looking perspective on its enduring influence on the future of the RE field. The central tenet of this review is that formal specifications are of limited value without scalable formal validation, a principle that Formal Tropos championed and that remains critically relevant today.