Introduction to software engineering -- Chapter 4 -- formal description technology

Introduction to software engineering —— Chapter four —— Formal description technology

1、 summary

According to the degree of formalization , The methods used in software engineering can be divided into Informal 、 Semi formal and formal Three types of . Describe the requirements specification naturally , It is a typical non formal method . Model with data flow diagram or entity relation diagram , It is a typical semi formal method . The so-called formal method , It is a mathematics based technology to describe the properties of the system , in other words , If a method has a solid mathematical foundation , Then it is formal .

2、 The disadvantages of non formal methods ：

1. contradiction ： A set of conflicting statements .
2. Two senses ： A statement that the reader can understand in different ways .
3. Ambiguity ： A general statement that does not specify any Ou Yong information .
4. Incompleteness ： A statement that does not specify a specific function .
5. Confusion of abstract levels ： It means that the non abstract statement is mixed with some low-level statements about details .

3、 The advantages of formal methods ：

1. Be able to describe Physical phenomena 、 An object or action Result . Accurate to almost no ambiguity , And it can be verified mathematically , To discover existing contradictions and incompleteness , There is no ambiguity in such specifications .
2. It can smoothly transition between different software engineering activities . Not only functional specifications , And the system design can also be expressed mathematically , Of course , Program code is also a mathematical symbol .
3. Provides a means of high-level confirmation , It can be proved mathematically , The design complies with the specifications , The program code correctly realizes the design result .

4、 Apply formal guidelines

1. Appropriate representation should be chosen .
2. It should be formalized , But don't over formalize
3. The cost should be estimated
4. There should be a formal method consultant to provide advice at any time
5. Traditional development methods should not be abandoned
6. Detailed documentation should be established
7. Quality standards should not be abandoned
8. We should not blindly rely on formal methods
9. It should be tested 、 Test and retest
10. Should reuse ： Even if the formal method is adopted , Software reuse is still the only reasonable way to reduce software cost and improve software quality , Moreover, the software components described by formal methods have clearly defined functions and interfaces , Make them more reusable .

5、 Finite state machines

Finite state machine is a formal method to express specification

A finite state machine consists of the following five parts ： State set J, Input set K, The next state is determined by the current state and the current input （ Substate ） The conversion function of T, The initial state S And the final state set F. A finite state machine can be expressed as a 5 Tuples （J、K、T、S、F）

give an example ：

In the above example ：

State set J：{ The safe is locked ,A,B, Safe unlocking , Call the police }

Input set K：{1L,1R,2L,2R,3L,3R}

Conversion function T：

Initial state S： The safe is locked .

The final set F:{ Safe unlocking , Call the police }

among :J Is a finite set of nonempty states ,K Is a finite nonempty input set ;T It is a slave. （J-F）* K To J The conversion function of ;S∈J, Is an initial state ,F Included in J, Is the final state set .

State transition

Each transition of state has the following form ：

current state [ menu ] + Time [ Selected The item ] =》 Next state

Expand

Make an extension to the finite state machine , That is, in the above 5 Add the... To the tuple 6 A component —— Predicate set P, Thus, the finite state machine is extended to a 6 Tuples , Each of these predicates is a global state Y Function of , Conversion function T Now it is a time from （J-F）* K * P To J Function of .

The current conversion rule is in the form of ：
current state [ menu ] + event [ Selected items ] + The predicate =》 Next state

advantage

• The finite state machine method manages a simple format to describe specifications ： current state + event + The predicate =》 Next state . This form of specification is easy to write 、 Easy to verify , And it can be easily transformed into design or program code .
• Finite state machine method is more accurate than data flow graph , And it's easy to understand .

shortcoming

• When developing large systems , A triple （ I.e. status 、 event 、 The predicate ） The number of will increase rapidly .
• The formal finite state machine method does not deal with timing requirements .

6、Petri network

（1） function

A major problem encountered in concurrent systems is Timing issues . Timing problems are usually caused by poor design or incorrect implementation . And such design or implementation is caused by poor specifications , If the specifications are not appropriate , There is a risk of incomplete design or implementation ,Petri A great advantage of net technology is that it can be used in design

（2） constitute

General composition ：
Petri The net contains 4 Elements ： A set of positions P、 A set of transformations T、 Input function I、 Output function O. Examples are as follows ：

• A set of positions P by {P1,p2,p3,p4}, Use a circle to represent the position in the figure .

• A set of transformations T by {T1,T2} Use a short line to represent the transformation in the figure

• Two input functions for conversion , Indicate by an arrow pointing to the transition for the chairman , They are I（t1） = {P2, P4}

  I(t2) = {P2}

• Two output functions for conversion , It is indicated by the arrow pointing to the position light from the conversion , They are ：O（t1） = {P1}

O(t2) = {P3, P4}

among ,P = {P1,……Pn} Is a finite location set

T = {t1,……,tm} Is a finite transformation set ,m>=0

（3） Assign token

① Marked Petri network

7、Z Language

use Z In words 、 The cheapest formal specification has the following four parts ：

（1） Given set

One Z The specification starts with a given set of initializations , An initialized set is a set that does not need to be defined in detail , This set is expressed in square brackets .

（2） State definition

One Z The specification consists of several “ grid ” form , Each lattice contains a set of variable descriptions and a series of predicates that limit the range of variable values .

（3） The initial state

The abstract initial state refers to the state when the system is first turned on .

（4） operation ：

1. When one cell is used in another cell , To prefix it with a triangle symbol 、 question mark ”?“ Represents the input variable , And exclamation marks ”！“ Represents the output variable
2. Predicate part , Contains a set of preconditions for invoking operations , And the post condition after the operation is completed , If the precondition holds , Then the post condition can be obtained after the operation is completed , however , If the operation is called when the precondition is not true , You cannot get the specified result .

Z The main reasons for the success of language are ：

1. It can be found easily Z Error in writing specifications , Especially when reviewing specifications , And review the design and code according to the formal specification , This is even more true .
2. Require very precise use of Z Specifiers write specifications . Reduced ambiguity 、 Inconsistencies and omissions .
3. Z Just a formal language , Developers can strictly verify the correctness of specifications when necessary .
4. Developers can learn to write in a relatively short time Z description
5. Use Z Language reduces the cost of software development by reducing the total time required for the development process
6. Users can base on Z The specification rewritten in natural language is clearer and more accurate than the informal specification written directly in natural language .

Is a formal language , Developers can strictly verify the correctness of specifications when necessary .
4. Developers can learn to write in a relatively short time Z description
5. Use Z Language reduces the cost of software development by reducing the total time required for the development process
6. Users can base on Z The specification rewritten in natural language is clearer and more accurate than the informal specification written directly in natural language .