A logic based approach to use case based requirement verification and domain model improvement

Abstract

In software systems, a significant number of software errors and disasters can be traced to late detection of requirements errors. Hence, it is crucial to concentrate on early design phases to verify the primary design against user requirements. In this thesis, two model based verification methods are proposed for performing early design verification and validation. The first approach is a predicate based verification method termed 'Predicate based Sequential Verification (PSV)' which checks the domain model against semi-formal Natural Language (NL) based Use Cases. The PSV module reports requirement violations and model inconsistencies and suggests improvements to the domain model. A proof based strategy termed 'Scenario Sequential Verification (SSV) Strategy' is also discussed as an alternative method for proving domain model requirements which relies on Program Transformation method using Hoare logic. The second verification approach called 'Semi-Automated Validation (SAV)' verifies the formal design model (state chart) against Semiformal NL based Use Case requirements.