Bài giảng Công nghệ phần mềm - Chương 4: Các kỹ thuật đặc tả

Các kꢀ thuꢁt ñꢂc tꢃ

(4)

Nguyꢀn Thanh Bình

Khoa Công nghꢁꢂThôngꢂtin

Trưꢃng ðꢄi hꢅc Bách khoa

ðꢄi hꢅc ðà Nꢆng

Nꢄi dung

ꢀ

Khái niꢅm ñꢂc tꢃ

Tꢆi sao phꢃi ñꢂc tꢃ ?

Phân loꢆi các kꢀ thuꢁt ñꢂc tꢃ

Các kꢀ thuꢁt ñꢂc tꢃ

2

1

Khái niꢅm ñꢂc tꢃ

ꢀ

ðꢂc tꢃ (specification)

ꢁ

ñꢇnh nghĩa mꢄt hꢅ thꢈng, mô-ñun hay

mꢄt sꢃn phꢉm cꢊn phꢃi làm cái gì

ꢁ

không mô tꢃ nó phꢃi làm như thꢋ nào

mô tꢃ nhꢌng tính chꢇt cꢈa vꢇn ñꢉꢍ

ñꢂt ra

ꢁ

không mô tꢃ nhꢌng tính chꢎt cꢏa giꢃi

pháp cho vꢎn ñꢐꢍñó

3

Khái niꢅm ñꢂc tꢃ

ꢀ

ðꢂc tꢃ là hoꢆt ñꢄng ñưꢑc tiꢋn hành trong

các giai ñoꢆn khác nhau cꢏa tiꢋn trình phꢊn

mꢐm:

ꢁ

ðꢂc tꢃ yêu cꢊu (requirement specification)

• sꢒ thꢈng nhꢎt giꢌa nhꢌng ngưꢓi sꢔ dꢕng tương

lai và nhꢌng ngưꢖi thiꢋt kꢋ

ꢁ

ðꢂc tꢃ kiꢋn trúc hꢅ thꢈng (system architect

specification)

• sꢒ thꢈng nhꢎt giꢌa nhꢌng ngưꢖi thiꢋt kꢋ và

nhꢌng ngưꢖi cài ñꢂt

ꢁ

ðꢂc tꢃꢍmôñunꢍ(module specification)

• sꢒ thꢈng nhꢎt giꢌa nhꢌng ngưꢖi lꢁp trình cài ñꢂt

mô-ñun và nhꢌng ngưꢖi lꢁp trình sꢔ dꢕng mô-ñun

4

2

Tꢆi sao phꢃi ñꢂc tꢃ ?

ꢀ

Hꢑp ñꢗng

sꢒ thꢈng nhꢎt giꢌa ngưꢖi sꢔ dꢕng vàꢍngưꢖi

phát triꢘn sꢃn phꢉm

Hꢑp thꢙc hóa

ꢁ

sꢃn phꢉm làm ra phꢃi thꢒc hiꢅn chính xác

nhꢌng gì mong muꢈn

Trao ñꢚi

ꢁ

giꢌa ngưꢖi sꢔ dꢕng vàꢍngưꢖi phát triꢘn

giꢌa nhꢌng ngưꢖi phát triꢘn

ꢁ

ꢀ

Tái sꢔ dꢕng

5

Phân loꢆi các kꢀ thuꢁt ñꢂc tꢃ

ꢀ

ðꢂc tꢃ phi hình thꢙc (informal)

ꢁ

ngôn ngꢌ tꢒ nhiên tꢒ do

ngôn ngꢌ tꢒ nhiên có cꢎu trúc

các kí hiꢅu ñꢗ hꢛa

ꢀ

ðꢂc tꢃ nꢌa hình thꢙc (semi-informal)

ꢁ

trꢄn lꢜn cꢃ ngôn ngꢌ tꢒ nhiên, các kí hiꢅu toán hꢛc và

các kí hiꢅu ñꢗ hꢛa

ðꢂc tꢃ hình thꢙc (formal)

ꢁ

kí hiꢅu toán hꢛc

• ngôn ngꢌꢍñꢂc tꢃ

• ngôn ngꢌ lꢁp trình

6

3

ðꢂc tꢃ hình thꢙc hay không

hình thꢙc ?

ꢀ

ðꢂc tꢃ hình thꢙc

ꢂ

ꢃ

chính xác (toán hꢛc)

hꢑp thꢙc hóa hình thꢙc (công cꢕ hóa)

công cꢕꢍtraoꢍñꢚi: khóꢍñꢛc, khó hiꢘu

khó sꢔ dꢕng

ꢀ

ðꢂc tꢃ không hình thꢙc

ꢂ

ꢃ

dꢝ hiꢘu, dꢝ sꢔ dꢕng

mꢐm dꢞo

thiꢋu sꢒ chính xác

nhꢁp nhꢟng

7

ꢠng dꢕng ñꢂc tꢃ hình thꢙc

ꢀ

ꢙng dꢕng trong các giai ñoꢆn sꢓm cꢏa tiꢋn

trình phát triꢘn

ꢀ

hꢆn chꢋ lꢡi trong phát triꢘn phꢊn mꢐm

ꢙng dꢕng chꢏ yꢋu trong phát triꢘn các hꢅ

thꢈng “quan trꢛng” (critical systems)

ꢁ

hꢅ thꢈng ñiꢐu khiꢘn

hꢅ thꢈng nhúng

hꢅ thꢈng thꢖi gian thꢒc

8

4

Chi phí phát triꢘn khi sꢔ

dꢕng ñꢂc tꢃ hình thꢙc

9

Các kꢀ thuꢁt ñꢂc tꢃ

ꢀ

Trình bày mꢄt sꢈ kꢀ thuꢁt

ꢁ

Máy trꢆng thái hꢌu hꢆn

Mꢆng Petri

ðiꢐu kiꢅn trưꢓc và sau

Kiꢘu trꢢu tưꢑng

ðꢂc tꢃ Z

10

5

Máy trꢆng thái hꢌu hꢆn

(state machine)

ꢀ

mô tꢃ các luꢗng ñiꢐu khiꢘn

biꢘu diꢝn dꢆng ñꢗ thꢇ

bao gꢗm

ꢁ

tꢁp hꢑp các trꢆng thái S (các nút cꢏa ñꢗ thꢇ)

ꢁ

tꢁp hꢑp các dꢌ liꢅu vào I (các nhãn cꢏa các

cung)

ꢁ

tꢁp hꢑp các chuyꢘn tiꢋp T : S x I → S (các

cung cóꢍhưꢓng cꢏa ñꢗ thꢇ)

• khi có mꢄt dꢌ liꢅu vào, mꢄt trꢆng thái chuyꢘn sang

mꢄt trꢆng thái khác

11

Máy trꢆng thái hꢌu hꢆn

ðꢑi

ðꢂt máy xuꢈng

ꢀ

Ví dꢕ 1

Nhꢎc máy

Âm mꢖi quay

sꢈ

Bꢎm sꢈ

Thꢖi gian ñꢑi kꢋt

thúc

Sꢈ sai

Thông báo

quay sꢈ sai

Quay sꢈ

Sꢈꢍñúng

Kꢋt nꢈi

Kꢋt nꢈi ñưꢑc

Máy bꢁn

ðꢚ chuông

Thuê bao ñưꢑc gꢛi nhꢎc máy

12

ðàm thoꢆi

6

Máy trꢆng thái hꢌu hꢆn

ꢀ

Ví dꢕ 2

ꢁ

Hꢅ thꢈng cꢊn mô tꢃ bao gꢗm mꢄt nhà sꢃn xuꢎt, mꢄt

nhà tiêu thꢕ và mꢄt kho hàng chꢣ chꢙa ñưꢑc nhiꢐu

nhꢎt 2 sꢃn phꢉm

ꢁ

Nhà sꢃn xuꢎt có 2 trꢆng thái

• P1: không sꢃn xuꢎt

• P2:ꢍñangꢍsꢃn xuꢎt

ꢁ

Nhà tiêu thꢕ có 2 trꢆng thái

• C1: có sꢃn phꢉm ñꢘ tiêu thꢕ

• C2: không có sꢃn phꢉm ñꢘ tiêu thꢕ

Nhà kho có 3 trꢆng thái

• chꢙa 0 sꢃn phꢉm

• chꢙa 1 sꢃn phꢉm

• chꢙa 2 sꢃn phꢉm

13

Máy trꢆng thái hꢌu hꢆn

ꢀ

Giꢃi pháp 1: mô tꢃ tách rꢖi các thành phꢊn

Lꢎy tꢢ kho

Sꢃn xuꢎt

P2

C2

P1

C1

Gꢔi vào kho

Tiêu thꢕ

Gꢔi vào kho

1

2

0

Lꢎy tꢢ kho

14

7

Máy trꢆng thái hꢌu hꢆn

ꢀ

Giꢃi pháp 1

ꢁ

không mô tꢃꢍñưꢑc sꢒ hoꢆt ñꢄng hꢅ

thꢈng

ꢁ

cꢊn mô tꢃ sꢒ hoꢆt ñꢄng kꢋt hꢑp các

thành phꢊn cꢏa hꢅ thꢈng

15

Máy trꢆng thái hꢌu hꢆn

ꢀ

Giꢃi pháp 2: mô tꢃ kꢋt hꢑp các thành phꢊn

<1, P1, C1>

<0, P1, C1>

<2, P1, C1>

Gꢔi vào kho

Sꢃn xuꢎt

Lꢎy tꢢ kho

Tiêu thꢕ

<1, P2, C1>

<1, P1, C2>

<2, P2, C1>

<2, P1, C2>

<0, P2, C1>

<0, P1, C2>

Lꢎy tꢢ kho

Tiêu thꢕ

Sꢃn xuꢎt

Gꢔi vào kho

<1, P2, C2>

<2, P2, C2>

<0, P2, C2>

16

8

Máy trꢆng thái hꢌu hꢆn

ꢀ

Giꢃi pháp 2

ꢂ

mô tꢃꢍñưꢑc hoꢆt ñꢄng cꢏa hꢅ thꢈng

ꢃ

sꢈ trꢆng thái lꢓn

biꢘu diꢝn hꢅ thꢈng phꢙc tꢆp

hꢆn chꢋ khiꢍñꢂc tꢃ nhꢌng hꢅ thꢈng không

ñꢗng bꢄ

o

các thành phꢊn cꢏa hꢅ thꢈng hoꢆt ñꢄng song

song hoꢂc cꢆnh tranh

17

Mꢆng Petri

(Petri nets)

ꢀ

thích hꢑp ñꢘ mô tꢃ các hꢅ thꢈng không

ñꢗng bꢄ vꢓi nhꢌng hoꢆt ñꢄng ñꢗng thꢖi

mô tꢃ luꢗng ñiꢐu khiꢘn cꢏa hꢅ thꢈng

ꢀ

ñꢐ xuꢎt tꢢꢍnămꢍ1962 bꢤi Carl Adam

Có hai loꢆi

ꢁ

mꢆng Petri (cꢚꢍñiꢘn)

mꢆng Petri mꢤ rꢄng

ꢁ

18

9

Mꢆng Petri

ꢀ

Gꢗm các phꢊn tꢔ

ꢁ

mꢄt tꢁp hꢑp hꢌu hꢆn các nút (ꢄ)

mꢄt tꢁp hꢑp hꢌu hꢆn các chuyꢀn tiꢁp (ꢅ)

mꢄt tꢁp hꢑp hꢌu hꢆn các cung (→)

• các cung nꢈi các nút vꢓi các chuyꢘn tiꢋp hoꢂc

ngưꢑc lꢆi

ꢁ

mꢡi nút có thꢘ chꢙa mꢄt hoꢂc nhiꢐu thꢂ (ꢁ)

19

Mꢆng Petri

ꢀ

Ví dꢕ

t2

t3

p2

p3

t1

p1

p4

20

10

Mꢆng Petri

ꢀ

Mꢆng Petri ñưꢑc ñꢇnh nghĩa bꢤi sꢒꢍñánh dꢎu các nút

cꢏa nó

Viꢅc ñánh dꢎu các nút ñưꢑc tiꢋn hành theo nguyên tꢥc

sau:

ꢁ

mꢡi chuyꢘn tiꢋp có các nút vào và các nút ra

ꢁ

nꢋu tꢎt cꢃ các nút vào cꢏa mꢄt chuyꢘn tiꢋp có ít nhꢎt

mꢄt thꢞ, thì chuyꢘn tiꢋp này là có thꢘ vưꢃt quaꢍñưꢑc,

ꢁ

nꢋu chuyꢘn tiꢋp này ñưꢑc thꢒc hiꢅn thì tꢎt cꢃ các nút

vào cꢏa chuyꢘn tiꢋp sꢦ bꢇ lꢎy ñi mꢄt thꢞ, và mꢄt thꢞ

sꢦꢍñưꢑc thêm vào tꢎt cꢃ các nút ra cꢏa chuyꢘn tiꢋp

nꢋu nhiꢐu chuyꢘn tiꢋp là có thꢘꢍvưꢑt qua thì chꢛn

chuyꢘn tiꢋp nào cũng ñưꢑc

21

Mꢆng Petri

ꢀ

Ví dꢕ

t1

t2

t1 không thꢊꢂvưꢋt qua ñưꢋc

t2 có thꢊꢂvưꢋt qua ñưꢋc

t3

hoꢌc t3ꢂñưꢋc vưꢋt qua

hoꢌc t4ꢂñưꢋc vưꢋt qua

t4

22

11

Mꢆng Petri

ꢀ

Ví dꢕ

t2

khi t2ꢂñưꢋc vưꢋt qua

23

Mꢆng Petri

Ví dꢕ

24

12

Mꢆng Petri

ꢀ

Ví dꢕ 1: mô tꢃ hoꢆt ñꢄng cꢏa ñèn giao thông

red

yr

yellow

green

rg

gy

25

Mꢆng Petri

ꢀ

Ví dꢕ 1: mô tꢃ hoꢆt ñꢄng cꢏa 2ꢍñèn giao thông

red2

red1

yr1

yr2

rg2

yellow1

green1

yellow2

rg1

gy2

gy1

26

green2

13

Mꢆng Petri

ꢀ

Ví dꢕ 1: mô tꢃ hoꢆt ñꢄng an toàn cꢏa 2ꢍñèn giao thông

red2

red1

safe

yr1

yr2

rg1

yellow2

rg2

yellow1

green1

gy1

gy2

27

green2

Mꢆng Petri

ꢀ

Ví dꢕ 1: mô tꢃ hoꢆt ñꢄng an toàn và hꢑp lý cꢏa 2ꢍñèn

giao thông

red1

red2

safe2

yr1

yr2

rg1

rg2

yellow1

green1

yellow2

gy2

gy1

safe1

28

green2

14

Mꢆng Petri

ꢀ

Ví dꢕ 2: mô tꢃ chu kỳ sꢈng cꢏa mꢄt ngưꢖi

trꢀ con

dꢃy thì

cưꢄi

có vꢁ có chꢂng

chꢅt

thanh niên

ly hôn

29

chꢅt

Mꢆng Petri

ꢀ

Ví dꢕ 3: viꢋt thư vàꢍñꢛc thư

begin

receive_mail

mail_box

rest

type_mail

read_mail

send_mail

ready

Mô tꢍꢂtrưꢃng hꢋp 1ꢂngưꢃi viꢎt vàꢂ2ꢂngưꢃi ñꢅc ?

Mô tꢍꢂtrưꢃng hꢋp hꢏp thư nhꢐn chꢑ chꢒa nhiꢉu nhꢇt 3ꢂthưꢂ?

30

15

Mꢆng Petri

ꢀ

Ví dꢕ 4: tình huꢈng nghꢦn (dead-lock)

P1

P2

P3

t1

t2

P4

P6

P5

P7

t3

t4

t5

t7

t6

t8

P8

P9

2

31

Mꢆng Petri

ꢀ

Ví dꢕ 4: giꢃi pháp chꢈng nghꢦn

P1

P2

P3

t1

t2

P4

P6

P5

P7

t3

t4

2

t5

t7

t6

t8

P8

P9

2

32

16

Mꢆng Petri

ꢀ

Ví dꢕ 5

ꢁ

Hꢅ thꢈng cꢊn mô tꢃ bao gꢗm mꢄt nhà sꢃn xuꢎt, mꢄt

nhà tiêu thꢕ và mꢄt kho hàng chꢣ chꢙa ñưꢑc nhiꢐu

nhꢎt 2 sꢃn phꢉm

ꢁ

Nhà sꢃn xuꢎt có 2 trꢆng thái

• P1: không sꢃn xuꢎt

• P2:ꢍñangꢍsꢃn xuꢎt

ꢁ

Nhà tiêu thꢕ có 2 trꢆng thái

• C1: có sꢃn phꢉm ñꢘ tiêu thꢕ

• C2: không có sꢃn phꢉm ñꢘ tiêu thꢕ

Nhà kho có 3 trꢆng thái

• chꢙa 0 sꢃn phꢉm

• chꢙa 1 sꢃn phꢉm

• chꢙa 2 sꢃn phꢉm

33

Mꢆng Petri

ꢀ

Ví dꢕ 5: mô tꢃ tách rꢖi mꢡi thành phꢊn

Sꢃn xuꢎt

Lꢎy tꢢ kho

C1

C2

P1

P2

Tiêu thꢕ

Gꢔi vào kho

1

2

0

Lꢎy tꢢ kho

34

17

Mꢆng Petri

ꢀ

Ví dꢕ 5: mô tꢃ kꢋt hꢑp các thành phꢊn

Sꢃn xuꢎt

P1

Gꢔi vào kho

P2

1

Gꢔi vào kho

Lꢎy tꢢ kho

2

0

Lꢎy tꢢ kho

C1

C2

Tiêu thꢕ

35

ðiꢐu kiꢅn trưꢓc và sau

(pre/post condition)

ꢀ

ñưꢑc dùng ñꢘꢍñꢂc tꢃ các hàm hoꢂc mô-ñun

ñꢂc tꢃ các tính chꢎt cꢏa dꢌ liꢅu trưꢓc và sau khi thꢒc

hiꢅn hàm

ꢁ

pre-condiition: ñꢂc tꢃ các ràng buꢄc trên các tham

sꢈ trưꢓc khi hàm ñưꢑc thꢒc thi

ꢁ

post-condition: ñꢂc tꢃ các ràng buꢄc trên các tham

sꢈ sau khi hàm ñưꢑc thꢒc thi

ꢀ

có thꢘ sꢔ dꢕng ngôn ngꢌ phi hình thꢙc, hình thꢙc

hoꢂc ngôn ngꢌ lꢁp trình ñꢘꢍñꢂc tꢃ các ñiꢐu kiꢅn

36

18

ðiꢐu kiꢅn trưꢓc và sau

ꢀ

Ví dꢕ: ñꢂc tꢃ hàm tìm kiꢋm

function search ( a : danh sách phꢊn tꢔ kiꢘu K,

size : sꢈ phân tꢔ cꢏa dánh sách,

e : phꢊn tꢔ kiꢘu K,

result : Boolean )

pre

i, 1 ≤ i ≤ n, a[i] ≤ a[i+1]

post

result = ( i, 1 ≤ i ≤ n, a[i] = e)

37

ðiꢐu kiꢅn trưꢓc và sau

ꢀ

Bài tꢁp:ꢍñꢂc tꢃ các hàm

1. Sꢥp xꢋp mꢄt danh sách các sꢈꢍnguyên

2. ðꢃo ngưꢑc các phꢊn tꢔ cꢏa mꢄt danh

sách

3. ðꢋm sꢈ phꢊn tꢔ có giá trꢇ e trong mꢄt danh

sách các sꢈ nguyên

38

19

Kiꢘu trꢢu tưꢑng

(abstract types)

ꢀ

Mô tꢃ dꢌ liꢅu và các thao tác trên dꢌ liꢅu ñó ꢤ mꢄt

mꢙc trꢢu tưꢑng ñꢄc lꢁp vꢓi cách cài ñꢂt dꢌ liꢅu bꢤi

ngôn ngꢌ lꢁp trình

ꢀ

ðꢂc tꢃ mꢄt kiꢘu trꢢu tưꢑng gꢗm:

ꢁ

tên cꢏa kiꢘu trꢢu tưꢑng

• dùng tꢢ khóa sort

khai báo các kiꢘu trꢢu tưꢑng ñã tꢗn tꢆi ñưꢑc sꢔ dꢕng

• dùng tꢢ khóa imports

các thao tác trên trên kiꢘu trꢢu tưꢑng

• dùng tꢢ khóa operations

39

Kiꢘu trꢢu tưꢑng

ꢀ

Ví dꢕ 1: ñꢂc tꢃ kiꢘu trꢢu tưꢑng Boolean

sort Boolean

operations

true

false

¬ _

: → Boolean

: Boolean → Boolean

: Boolean x Boolean → Boolean

_

mꢏt thao tác không có tham sꢔ là mꢏt hꢕng sꢔ

mꢏt giá trꢖ cꢈa kiꢊu trꢗu tưꢋng ñꢖnh nghĩa ñưꢋc biꢊu diꢀn bꢘi kí tꢙ “_”

40

20

Bài giảng Công nghệ phần mềm - Chương 4: Các kỹ thuật đặc tả - Nguyễn Thanh Bình