Lectures Software Engineering - Chapter 9: Formal Specification

40 trang hoanguyen 2900

Download

Bạn đang xem 20 trang mẫu của tài liệu "Lectures Software Engineering - Chapter 9: Formal Specification", để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên

Tài liệu đính kèm:

lectures_software_engineering_chapter_9_formal_specification.ppt

Nội dung text: Lectures Software Engineering - Chapter 9: Formal Specification

Formal Specification l Techniques for the unambiguous specification of software ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 1
Objectives l To explain why formal specification techniques help discover problems in system requirements l To describe the use of algebraic techniques for interface specification l To describe the use of model-based techniques for behavioural specification ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 2
Topics covered l Formal specification in the software process l Interface specification l Behavioural specification ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 3
Formal methods l Formal specification is part of a more general collection of techniques that are known as ‘formal methods’ l These are all based on mathematical representation and analysis of software l Formal methods include • Formal specification • Specification analysis and proof • Transformational development • Program verification ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 4
Acceptance of formal methods l Formal methods have not become mainstream software development techniques as was once predicted • Other software engineering techniques have been successful at increasing system quality. Hence the need for formal methods has been reduced • Market changes have made time-to-market rather than software with a low error count the key factor. Formal methods do not reduce time to market • The scope of formal methods is limited. They are not well- suited to specifying and analysing user interfaces and user interaction • Formal methods are hard to scale up to large systems ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 5
Use of formal methods l Formal methods have limited practical applicability l Their principal benefits are in reducing the number of errors in systems so their mai area of applicability is critical systems l In this area, the use of formal methods is most likely to be cost-effective ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 6
Specification in the software process l Specification and design are inextricably intermingled. l Architectural design is essential to structure a specification. l Formal specifications are expressed in a mathematical notation with precisely defined vocabulary, syntax and semantics. ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 7
Specification techniques l Algebraic approach • The system is specified in terms of its operations and their relationships l Model-based approach • The system is specified in terms of a state model that is constructed using mathematical constructs such as sets and sequences. Operations are defined by modifications to the system’s state ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 10
Use of formal specification l Formal specification involves investing more effort in the early phases of software development l This reduces requirements errors as it forces a detailed analysis of the requirements l Incompleteness and inconsistencies can be discovered and resolved l Hence, savings as made as the amount of rework due to requirements problems is reduced ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 12
Interface specification l Large systems are decomposed into subsystems with well-defined interfaces between these subsystems l Specification of subsystem interfaces allows independent development of the different subsystems l Interfaces may be defined as abstract data types or object classes l The algebraic approach to formal specification is particularly well-suited to interface specification ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 14
Specification components l Introduction • Defines the sort (the type name) and declares other specifications that are used l Description • Informally describes the operations on the type l Signature • Defines the syntax of the operations in the interface and their parameters l Axioms • Defines the operation semantics by defining axioms which characterise behaviour ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 17
Systematic algebraic specification l Algebraic specifications of a system may be developed in a systematic way • Specification structuring. • Specification naming. • Operation selection. • Informal operation specification • Syntax definition • Axiom definition ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 18
Specification operations l Constructor operations. Operations which create entities of the type being specified l Inspection operations. Operations which evaluate entities of the type being specified l To specify behaviour, define the inspector operations for each constructor operation ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 19
Operations on a list ADT l Constructor operations which evaluate to sort List • Create, Cons and Tail l Inspection operations which take sort list as a parameter and return some other sort • Head and Length. l Tail can be defined using the simpler constructors Create and Cons. No need to define Head and Length with Tail. ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 20
Recursion in specifications l Operations are often specified recursively l Tail (Cons (L, v)) = if L = Create then Create else Cons (Tail (L), v) • Cons ([5, 7], 9) = [5, 7, 9] • Tail ([5, 7, 9]) = Tail (Cons ( [5, 7], 9)) = • Cons (Tail ([5, 7]), 9) = Cons (Tail (Cons ([5], 7)), 9) = • Cons (Cons (Tail ([5]), 7), 9) = • Cons (Cons (Tail (Cons ([], 5)), 7), 9) = • Cons (Cons ([Create], 7), 9) = Cons ([7], 9) = [7, 9] ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 22
Interface specification in critical systems l Consider an air traffic control system where aircraft fly through managed sectors of airspace l Each sector may include a number of aircraft but, for safety reasons, these must be separated l In this example, a simple vertical separation of 300m is proposed l The system should warn the controller if aircraft are instructed to move so that the separation rule is breached ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 23
A sector object l Critical operations on an object representing a controlled sector are • Enter. Add an aircraft to the controlled airspace • Leave. Remove an aircraft from the controlled airspace • Move. Move an aircraft from one height to another • Lookup. Given an aircraft identifier, return its current height ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 24
Primitive operations l It is sometimes necessary to introduce additional operations to simplify the specification l The other operations can then be defined using these more primitive operations l Primitive operations • Create. Bring an instance of a sector into existence • Put. Add an aircraft without safety checks • In-space. Determine if a given aircraft is in the sector • Occupied. Given a height, determine if there is an aircraft within 300m of that height ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 25
Sector specification
Specification commentary l Use the basic constructors Create and Put to specify other operations l Define Occupied and In-space using Create and Put and use them to make checks in other operation definitions l All operations that result in changes to the sector must check that the safety criterion holds ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 27
Behavioural specification l Algebraic specification can be cumbersome when the object operations are not independent of the object state l Model-based specification exposes the system state and defines the operations in terms of changes to that state l The Z notation is a mature technique for model- based specification. It combines formal and informal description and uses graphical highlighting when presenting specifications ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 28
Modelling the insulin pump l The schema models the insulin pump as a number of state variables • reading? • dose, cumulative_dose • r0, r1, r2 • capacity • alarm! • pump! • display1!, display2! l Names followed by a ? are inputs, names followed by a ! are outputs ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 31
Schema invariant l Each Z schema has an invariant part which defines conditions that are always true l For the insulin pump schema it is always true that • The dose must be less than or equal to the capacity of the insulin reservoir • No single dose may be more than 5 units of insulin and the total dose delivered in a time period must not exceed 50 units of insulin. This is a safety constraint (see Chapters 16 and 17) • display1! shows the status of the insulin reservoir. ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 32
The dosage computation l The insulin pump computes the amount of insulin required by comparing the current reading with two previous readings l If these suggest that blood glucose is rising then insulin is delivered l Information about the total dose delivered is maintained to allow the safety check invariant to be applied l Note that this invariant always applies - there is no need to repeat it in the dosage computation ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 34
Output schemas l The output schemas model the system displays and the alarm that indicates some potentially dangerous condition l The output displays show the dose computed and a warning message l The alarm is activated if blood sugar is very low - this indicates that the user should eat something to increase their blood sugar level ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 36
Schema consistency l It is important that schemas are consistent. Inconsistency suggests a problem with the system requirements l The INSULIN_PUMP schema and the DISPLAYare inconsistent • display1! shows a warning message about the insulin reservoir (INSULIN_PUMP) • display1! Shows the state of the blood sugar (DISPLAY) l This must be resolved before implementation of the system ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 38
Key points l Formal system specification complements informal specification techniques l Formal specifications are precise and unambiguous. They remove areas of doubt in a specification l Formal specification forces an analysis of the system requirements at an early stage. Correcting errors at this stage is cheaper than modifying a delivered system ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 39
Key points l Formal specification techniques are most applicable in the development of critical systems and standards. l Algebraic techniques are suited to interface specification where the interface is defined as a set of object classes l Model-based techniques model the system using sets and functions. This simplifies some types of behavioural specification ©Ian Sommerville 2000 Software Engineering, 6th edition. Chapter 9 Slide 40