Formal Specification

Formal Specification
Dr.ShaneMatts Profile Pic
Dr.ShaneMatts,United States,Teacher
Published Date:23-07-2017
Your Website URL(Optional)
Comment
Chapter 10 Formal Specification ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 1Objectives  To explain why formal specification helps discover problems in system requirements.  To describe the use of:  Algebraic specification techniques, and  Model-based specification techniques (including simple pre- and post-conditions). ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 2Formal methods  Formal specification is part of a more general collection of techniques known as “formal methods.”  All are based on the mathematical rep- resentations and analysis of requirements and software. ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 3Formal methods (cont’d)  Formal methods include:  Formal specification (e.g., “model  Specification analysis and property proofs checking”)  Transformational development  Program verification (program correctness (axiomatic, function theoretic) proofs)  Specifications are expressed with precisely defined vocabulary, syntax, and semantics. ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 4Acceptance and use  Formal methods have not become main-stream as was once predicted, especially in the US. Some reasons why: 1. Less costly techniques (e.g., inspections / reviews) have been successful at increasing system quality. (Hence, the need for formal methods has been reduced.) (Cont’d) ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 5Acceptance and use (cont’d) 2. Market changes have made time-to- market rather than quality the key issue for many systems. (Formal methods do not reduce time-to- market.) 3. Limited scope of formal methods. They’re not well-suited to specifying user interfaces. (Many interactive applications are “GUI-heavy” today.) (Cont’d) ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 6Acceptance and use (cont’d) 4. Formal methods are hard to scale up for very large systems. (Although this is rarely necessary.) 5. Start-up costs are high. 6. Thus, the risks of adopting formal methods on most projects outweigh the benefits. ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 7Acceptance and use (cont’d)  However, formal specification is an excellent way to find (at least some types of) requirements errors and to express requirements unambiguously.  Projects which use formal methods invariably report fewer errors in the delivered software. ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 8Acceptance and use (cont’d)  In systems where failure must be avoided, the use of formal methods is justified and likely to be cost-effective.  Thus, the use of formal methods is increasing in critical system development where safety, reliability, and security are important. ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 9Formal specification in the software process Requirements Formal specification specification Requirements High-level definition design elicitation System Architectural modelling design a “back-end” element of requirements elicitation/analysis/specification/validation ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 10Formal specification techniques  Algebraic approach – system is specified in terms of its operations and their relationships via axioms.  Model-based approach (including simple pre- and post-conditions) – system is specified in terms of a state model and operations are defined in terms of changes to system state. ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 11Formal specification languages Sequential Concurrent Algebraic Larch (Guttag, Horning et Lotos (Bolognesi and al., 1985; Guttag, Brinksma, 1987), Horning et al., 1993), OBJ (Futatsugi, Goguen et al., 1985) Model-based Z (Spivey, 1992) CSP (Hoare, 1985) VDM (Jones, 1980) Petri Nets (Peterson, B (Wordsworth, 1996) 1981) ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 12Use of formal specification  Formal specification is a rigorous process and requires more effort in the early phases of software development.  This reduces requirements errors as ambiguities, incompleteness, and inconsistencies are discovered and resolved.  Hence, rework due to requirements problems is greatly reduced. ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 13Development costs with formal specification Cost Validation Design and Implementation Validation Design and Implementation Specification Specification Without formal With formal specification specification ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 14Algebraic Specification of sub-system interfaces  Large systems are normally comprised of sub-systems with well-defined interfaces.  Specification of these interfaces allows for their independent development.  Interfaces are often defined as abstract data types (“sorts”) or objects.  The algebraic approach is particularly well- suited to the specification of such interfaces. ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 15Sub-system interfaces Interface objects Sub-system Sub-system A B ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 16The structure of an algebraic specification SPECIFICATION NAME (Gener ic Parameter) sort name imports LIST OF SPECIFICATION NAMES Informal description of the sor t and its operations Operation signatures setting out the names and the types of the parameters to the operations defined over the sort Axioms defining the operations over the sort ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 17Algebraic specification components  Introduction – defines the sort (type name) and declares other specifications that are used  Description – informally describes the operations on the type  Signature – defines the syntax of the operations in the interface and their parameters  Axioms – defines the operation semantics by defining axioms which characterize behavior ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 18Types of operations  Constructor operations: operations which create / modify entities of the type  Inspection operations: operations which evaluate entities of the type being specified  Rule of thumb for defining axioms: define an axiom which sets out what is always true for each inspection operation over each (primitive) constructor operation. ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 19Operations on a (FIFO linear) “List” abstract data type  Constructor operations which create or modify sort List: Create, Cons and Tail  Inspection operations which discover attributes of sort List: Head and Length (LISP fans: Tail = CDR, Head = CAR)  Tail is not a primitive operation since it can be defined using Create and Cons. (Thus, axioms are not required for Head and Length over Tail.) ©Ian Sommerville 2000 Software Engineering, Chapter 10 Slide 20

Advise: Why You Wasting Money in Costly SEO Tools, Use World's Best Free SEO Tool Ubersuggest.