Identifying the Suitability of Any Formal Language for a Particular Application Area

Abstract

Formal Specification of a system has been an active area of research since past few decades. In software engineering, the formal specification of requirement phase is of most importance to achieve rigorous development and maintenance of software systems. Conventional software engineering based on in formal or semi-formal methods are facing challenges in ensuring software productivity and quality. Formal methods have attempted to address those challenges by introducing mathematical notation and calculus to support formal specification, refinement and verification in software development. Despite of their theoretical potential in improving the controllability of software process and reliability, formal methods are difficult to apply to large scale and complex systems in industry due to various practical constraints. For example, limited expertise, time and budget restrictions, etc. Since formal methods are based on mathematics and logic, they can be used for specifying and verifying both hardware and software systems. By using the formal methods, one can minimize the ambiguity and uncertainty inherent in natural language specifications. Once specified formally, a design can be mathematically verified against user requirements. By making this verification process, the implementation of complex and safety-critical system becomes much more credible. This thesis report suggests which formal specification language is suitable for particular type of problem e.g. communication type problems, real time application, and problems involving concurrency etc. There are a number of formal specification languages, Z, VDM, OCL, SDL etc. This thesis report basically compiles analysis of various formal specification languages and case studies, based on which the best suited formal language for a particular area of application is concluded.