tailieunhanh - Lecture Formal methods in software engineering: Formal specification

After studying this chapter you will be able to: To explain why formal specification techniques help discover problems in system requirements, to describe the use of algebraic techniques for interface specification, to describe the use of model-based techniques for behavioural specification. | Formal Methods in Software Engineering Credit Hours: 3+0 By: Qaisar Javaid Assistant Professor Objectives To explain why formal specification techniques help discover problems in system requirements To describe the use of algebraic techniques for interface specification To describe the use of model-based techniques for behavioural specification Topics covered Formal specification in the software process Sub-system interface specification Behavioural specification Interface specification in critical systems Consider an air traffic control system where aircraft fly through managed sectors of airspace. Each sector may include a number of aircraft but, for safety reasons, these must be separated. In this example, a simple vertical separation of 300m is proposed. The system should warn the controller if aircraft are instructed to move so that the separation rule is breached. A sector object 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; Primitive operations It is sometimes necessary to introduce additional operations to simplify the specification. The other operations can then be defined using these more primitive operations. 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. Sector specification (1) Sector specification (2) Specification commentary Use the basic constructors Create and Put to specify other operations. Define Occupied and In-space using Create and Put and use them to make checks in other operation definitions. All operations that result in changes to the sector must check that the safety criterion . | Formal Methods in Software Engineering Credit Hours: 3+0 By: Qaisar Javaid Assistant Professor Objectives To explain why formal specification techniques help discover problems in system requirements To describe the use of algebraic techniques for interface specification To describe the use of model-based techniques for behavioural specification Topics covered Formal specification in the software process Sub-system interface specification Behavioural specification Interface specification in critical systems Consider an air traffic control system where aircraft fly through managed sectors of airspace. Each sector may include a number of aircraft but, for safety reasons, these must be separated. In this example, a simple vertical separation of 300m is proposed. The system should warn the controller if aircraft are instructed to move so that the separation rule is breached. A sector object Critical operations on an object representing a controlled sector are Enter. Add an aircraft to the