©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 1Formal Specificationz Techniques for the unambiguous specification of software©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 2Specification in the Software Processz Specification and design are intermingled.z Architectural design is essential to structure a specification.z Formal specifications are expressed in a mathematical notation with precisely defined vocabulary, syntax and semantics.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 3Specification and DesignArchitecturaldesignRequirementsspecificationRequirementsdefinitionSoftwarespecificationHigh-leveldesignIncreasing contractor involvementDecreasing client involvementSpecificationDesign©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 4Formal Specification on Trialz Formal techniques are not widely used in industrial software development.z Given the relevance of mathematics in other engineering disciplines, why is this the case?©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 5Why Aren’t Formal Methods Used?z Inherent management conservatism. It is hard to demonstrate the advantages of formal specification in an objective way.z Many software engineers lack the training in discrete math necessary for formal specification.z System customers may be unwilling to fund specification activities.z Some classes of software (particularly interactive systems and concurrent systems) are difficult to specify using current techniques.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 6Why Aren’t Formal Methods Used?z There is widespread ignorance of the applicability of formal specifications.z There is little tool support available for formal notations.z Some computer scientists who are familiar with formal methods lack knowledge of the real-world problems to which these may be applied and therefore oversell the technique.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 7Advantages of Formal Specificationz It provides insights into the software requirements and the design. z Formal specifications may be analyzed mathematically for consistency. z It may be possible to prove that the implementation satisfies the specification. ©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 8Advantages of Formal Specificationz Formal specifications may be used to guide the tester of the component in identifying appropriate test cases.z Formal specifications may be processed using software tools. It may be possible to animate the specification to provide a software prototype.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 9Seven Myths of Formal Methodsz Perfect software results from formal methods– Nonsense - the formal specification is a model of the real-world and may incorporate misunderstandings, errors and omissions.z Formal methods means program proving– Formally specifying a system is valuable without formal program verification as it forces a detailed analysis early in the development process.z Formal methods can only be justified for safety-critical systems.– Industrial experience suggests that the development costs for all classes of system are reduced by using formal specification.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 10Seven Myths of Formal Methodsz Formal methods are for mathematicians– Nonsense - only simple math is needed.z Formal methods increase development costs– Not proven. However, formal methods definitely push development costs towards the front-end of the life cycle.z Clients cannot understand formal specifications– They can if they are paraphrased in natural language.z Formal methods have only been used for trivial systems– There are now many published examples of experience with formal methods for non-trivial software systems.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 11The Verdict!z The reasons put forward for not using formal specifications and methods are weak.z However, there are good reasons why these methods are not used:– The move to interactive systems. Formal specification techniques cannot cope effectively with graphical user interfacespecification.– Successful software engineering. Investing in other software engineering techniques may be more cost-effective.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 12Use of Formal Methodsz These methods are unlikely to be widely used in the foreseeable future. Nor are they likely to be cost-effective for most classes of system.z They will become the normal approach to the development of safety critical systems and standards.z This changes the expenditure profile through the software process.©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 13Development Costs with Formal SpecificationSpecificationDesign andImplementationValidationSpecificationDesign andImplementationValidationCostWithout formalspecificationWith formalspecification©Ian Sommerville 1995/2000 (Modified by Spiros Mancoridis 1999) Software Engineering, 6th edition. Chapter 9 Slide 14Specifying Functional Abstractionsz The simplest specification is function specification. There is no need to be concerned with global state.z The formal specification is expressed as input and output predicates (pre and post conditions).z Predicates are logical expressions which are always either true or false .z Predicate operators include the usual logical