A systematic approach to transforming system requirements into model checking specifications
Daniel Aceituna, Hyunsook Do, Sudarshan K. Srinivasan · 2014
We propose a method that addresses the following dilemma: model checking can formally expose off-nominal behaviors and unintended scenarios in the requirements of concurrent reactive systems. Requirements engineers and non-technical stakeholders who are the system domain experts can greatly benefit from jointly using model checking during the elicitation, analysis, and verification of system requirements. However, model checking is formal verification and many requirements engineers and domain experts typically lack the knowledge and training needed to apply model checking to the formal verification of requirements. To get full advantages of model checking and domain experts’ knowledge in verifying the system, we proposed a front end framework to model checking and evaluated our approach using a real world application.