Lec 11-Formal Specifications
Objectives:
- To explain why formal specification techniques help discover problems in system requirements
- Todescribe the use of:
- algebraic techniques(for interface specification)
- model-based techniques(for behavioural specification)
- To introduce Abstract State Machine model(ASML)
Formal Methods
- Formal specification is part of a more general collection of techniques that are known as ‘formal methods’
- Formal methods include
- Formal specification
- Specification analysis and proof
- Transformational development
- Program verification
Formal Method in reality
- When software was first developed
- it was done using assembly language
- No OO, no high level languages
- Limited understanding of software testing and testing tools
- Modern software development
- Many ways to make high quality software
Acceptance of Formal Methods
- Formal methods have not become mainstream software development techniques as was once predicted
Use of Formal Methods
Specification in the software process
- Specification and design are inextricably mixed.
- Architectual design is essential to structure a specification
- Formal specifications are expressed in mathematical notation with precisely defined vocabulary, syntax and Semantic
Specification Techniques
Use of Formal Specification
- 正式的规范要求在软件开发的早期阶段投入更多的精力
- 这减少了需求错误，因为它迫使对需求进行详细的分析
- 不完整性和不一致性可以被发现和解决。
- 因此，由于需求问题导致的返工数量减少，从而节省了成本
Formal Specification
- 系统需求和设计被详细地表达出来，减少歧义，并在实现开始前仔细地分析和细化
- 形式化规范的一大好处是它能够发现需求中的潜在问题和歧义。
Interface Specification
- 大型系统被分解为子系统，这些子系统之间有定义良好的接口
- 子系统接口的规范允许不同子系统的独立开发
- 接口可能被定义成 抽象数据类型 或者 事物类
形式规范的代数方法特别适合于接口规范
Sub-system Interface Specification
The Strucutre of an Algebraic Specification
- Introduction - Declare the sort(the type name) of the entity being specified, i.e., a set of objects with common characteristics. It also imports other specifications to use.
- Description - An informal description of the operations
to aid understanding. - Signature - Defines the syntax of the interface to the abstract data type(object), including their names, parameters list and return types.
- Axioms(公理) - Defines the semantics of the operations by defining axioms characterising the behaviour
Systematic Algebraic Specification
- Algebraic specifications of a system may be deceloped in a systematic way:
- Specification structuring;
- Specification naming
- operation selection
- Informal operation specification
- Syntax definition
- Axiom definition
Specification Operations
- Constructor operations Operations which create entities of thetype being specified.
- Inspection operations Operations which evaluate entites of the type being specified
- To specify behaviour, define the snspector operations for each constructor operation
- Example: Operation on a List ADT
Interface Specification in Critical Systems
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 the 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.
Speification Commentary for Sector
