1
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
2
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
3
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 ñề ñó
4
Khái niệm ñặc tả


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
6
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
4


ứ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
5
9
Chi phí phát triển khi sử
dụng ñặc tả hình thức
10
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
6
11
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ị

Thông báo
quay số sai
Số ñúng
Số sai
Bấm số
Kết nối ñược
7
13
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
14
Máy trạng thái hữu hạn

Lấy từ kho
Gửi vào kho
Tiêu thụ
Tiêu thụ
Sản xuất
Sản xuất
<0, P2, C2>
<0, P2, C1>
<0, P1, C2>
<0, P1, C1>
Tiêu thụ
Tiêu thụ
Sản xuất
Sản xuất
<1, P2, C2>
<1, P2, C1>
<1, P1, C2>
<1, P1, C1>
Tiêu thụ
Tiêu thụ
Sản xuất
Sản xuất
<2, P2, C2>
<2, P2, C1>
<2, P1, C2>
<2, P1, C1>
Lấy từ kho
Gửi vào kho
Lấy từ kho
Gửi vào kho

mạng Petri (cổ ñiển)

mạng Petri mở rộng
10
19
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ẻ ()
20
Mạng Petri

Ví dụ
t2
p1
p2
p3
p4
t3
t1
11

hoặc t4 ñược vượt qua
12
23
Mạng Petri

Ví dụ
khi t2 ñược vượt qua
t2t2
24
Mạng Petri
Ví dụ
13
25
Mạng Petri

Ví dụ 1: mô tả hoạt ñộng của ñèn giao thông
rg
red
yellow
green
yr
gy
26
Mạng Petri

Ví dụ 1: mô tả hoạt ñộng của 2 ñèn giao thông
rg1
red1
yellow1
green1

giao thông
rg1
red1
yellow1
green1
yr1
gy1
rg2
red2
yellow2
green2
yr2
gy2
safe2
safe1
15
29
Mạng Petri

Ví dụ 2: mô tả chu kỳ sống của một người
thanh niên
trẻ con
có vợ có chồng
dậy thì
cưới
ly hôn
chết chết
30
Mạng Petri


P9
t2
t4
t6
t8
32
22
Mạng Petri

Ví dụ 4: giải pháp chống nghẽn
22
P6
P4
P3
P1
P8
t1
t3
t5
t7
P7
P5
P2
P9
t2
t4
t6
t8
17
33

Tiêu thụ
C2
0
Gửi vào kho
1
2
Gửi vào kho
Lấy từ khoLấy từ kho
18
35
Lấy từ kho
Mạng Petri

Ví dụ 5: mô tả kết hợp các thành phần
Lấy từ kho
Gửi vào kho
Gửi vào kho
P1
Sản xuất
P2
0 1
2
C2
C1
Tiêu thụ
36
ðiều kiện trước và sau
(pre/post condition)

ñược dùng ñể ñặc tả các hàm hoặc mô-ñun

ðả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
20
39
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
40
Kiểu trừu tượng

Ví dụ 1: ñặc tả kiểu trừu tượng Boolean
sort Boolean
operations

true : →
→→
→ Boolean
false : →
→→
→ Boolean
¬
¬¬
¬ _ : Boolean →
→→
→ Boolean
_ ∧
∧∧
∧ _ : Boolean x 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ự “_”
42
Kiểu trừu tượng

Ví dụ 2: ñặc tả kiểu trừu tượng Vector
sort Vector
imports Integer, Element, Boolean
operations

• dùng từ khóa axioms

ñịnh nghĩa các ràng buộc mà một thao tác
ñược ñịnh nghĩa
• dùng từ khóa precondition
44
Kiểu trừu tượng

Ví dụ 2: ñặc tả kiểu trừu tượng Vector
precondition
ith(v, i) is-defined-ifonlyif
infborder(v) ≤
≤≤
≤ i ≤
≤≤
≤ supborder(v) &
&&
& init(v,i) = true
axioms
infborder(v) ≤
≤≤
≤ i ≤
≤≤
≤ supborder(v) ⇒
⇒⇒
⇒ ith(change-ith(v, i, e), i) = e
infborder(v) ≤
≤≤
≤ i ≤
≤≤

≠ j ⇒
⇒⇒
⇒ init(change-ith(v, i, e), j) = init(v, j)
infborder(vect(i, j)) = i
infborder(change-ith(v, i, e)) = infborder(v)
supborder(vect(i, j)) = j
supborder(change-ith(v, i, e)) = supborder(v)
with
v: Vector; i, j, k: Integer; e: Element
23
45
Kiểu trừu tượng

Bài tập

ðặc tả kiểu trừu tượng cây nhị phân

ðặc tả kiểu trừu tượng tập hợp