Formal Specification and Validation using a Scenario-Based Approach: The GPRS Group-Call Example
Daniel Amyot, Neil Darren. Hart, Pascal Forhan · 1997
Deriving a formal specification and a detailed design from informal requirements can be a tedious and error-prone task unless a methodical or rigorous approach is used. An increasing number of designers are interested in scenariodriven approaches that allow them to focus on the main functional aspects of the system to be specified. We present an approach where informal requirements are described with a use case notation called Use Case Map, and formal specifications and test cases are written in the process-algebraic language LOTOS. We present the approach by using an example: a Group Call service of the mobile data system GPRS. This work also aims to present ideas on how to integrate LOTOS and Use Case Maps in the ROOM methodology, and to discuss several strategies for scenario-based validation.