Use Case based Requirements
Formalization and Verification System (UCFV)
Abstract: This presentation is oriented towards analyzing and formalizing the use cases at the very early stages of software development. Many requirement errors are detected at the implementation phase and these errors could lead to software economic crisis at later development stages. It is crucial to concentrate more on early requirement analysis and design phases to understand and analyze the requirements exactly as demanded by the user. The above is possible, only if a proper methodology for requirements elicitation and the constructed requirement model is guaranteed to prove the requirements logically. Our approach consists of two phases--- 1. We introduce a semi validation method for associating the informal requirements which is in the shape of a semi-formal use case state chart, obtained as the final result of UCed (Stephane Some) tool, to the formal requirements in the form of OCL operations. 2. Providing an interface to the first phase for mathematical proving of these OCL conditions by converting them to first order logic and prove using Isabelle theorem prover. Thus the proving phase helps to understand that the system is free of any use case conflicts and ambiguities. Also, a similar technology for bridging object oriented development techniques and formal methods is described through the “KeY” project developed for smart card applications, in the concluding part of the discussion.