Công nghệ phần mềm - Các kỹ thuật đặc tả

pdf

23 trang vanle 2470

Download

Bạn đang xem 20 trang mẫu của tài liệu "Công nghệ phần mềm - Các kỹ thuật đặc tả", để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên

Tài liệu đính kèm:

cong_nghe_phan_mem_cac_ky_thuat_dac_ta.pdf

Nội dung text: Công nghệ phần mềm - 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ơngtin Tr ưng ði h c Bách khoa ði h c ðà Nng Ni dung Khái ni m đc t Ti 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 mt 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 đon khác nhau c a ti n trình ph n mm: ðc t yêu c u (requirement specification) • s th ng nh t gi a nh ng ng ưi s dng 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 dng mơ-đun 4 2
Ti sao ph i đc t ? Hp đng s th ng nh t gi a ng ưi s dng vàngưi phát tri n s n ph m Hp th c hĩa sn 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 dng vàngưi phát tri n gi a nh ng ng ưi phát tri n Tái s dng 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ĩ cu trúc các kí hi u đ ha ðc t na hình th c (semi-informal) tr n l n c ngơn ng t nhiên, các kí hi u tốn h c và các kí hi u đ ha ðc t hình th c (formal) kí hi u tốn h c • ngơn ng đc t • ngơn ng lp 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 (tốn h c) hp 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 dng ðc t khơng hình th c d hi u, d s dng mm 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 đon s m c a ti n trình phát tri n hn ch li trong phát tri n ph n m m ng d ng ch yu trong phát tri n các h th ng “quan tr ng” (critical systems) h th ng điu 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 dng đ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 Mng Petri ðiu 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 điu khi n bi u di n d ng đ th bao g m tp h p các tr ng thái S (các nút c a đ th ) tp h p các d li u vào I (các nhãn c a các cung) tp h p các chuy n ti p T : S x I → S (các cung cĩhưng ca đ th ) • khi cĩ mt d li u vào, m t tr ng thái chuy n sang mt tr ng thái khác 11 Máy tr ng thái h u h n ðt máy xu ng ði ðt máy xu ng Ví d 1 Nh c máy Âm m i quay s Th i gian đi k t Bm s thúc S sai Thơng báo Quay s quay s sai Sđ úng Kt n i Máy b n Kt n i đưc ð 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à sn xu t, m t nhà tiêu th và mt kho hàng ch ch a đưc nhi u nh t 2 s n ph m Nhà sn xu t cĩ 2 tr ng thái • P1: khơng s n xu t • P2: đangsn xu t Nhà tiêu th cĩ 2 tr ng thái • C1: cĩ sn ph m đ tiêu th • C2: khơng cĩ sn 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 Sn xu t Ly t kho P1 P2 C1 C2 Gi vào kho Tiêu th Gi vào kho Gi vào kho 0 1 2 Ly t kho Ly 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 cn 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 kt h p các thành ph n Gi vào kho Gi vào kho Sn xu t Sn xu t Sn xu t Ly t kho Ly t kho Tiêu th Tiêu th Tiêu th Ly t kho Ly t kho Tiêu th Tiêu th Tiêu th Sn xu t Sn xu t Sn xu t Gi vào kho Gi vào kho 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 hn 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 Mng Petri (Petri nets) thích hp đ mơ t các h th ng khơng đng b vi nh ng ho t đng đng th i mơ t lu ng điu khi n c a h th ng đ xu t t năm 1962 b i Carl Adam Cĩ hai lo i mng Petri (c đin) mng Petri m rng 18 9
Mng Petri Gm các ph n t mt t p h p hu hn các nút () mt t p h p hu hn các chuy n ti p () mt t p h p hu hn các cung (→) • các cung ni các nút v i các chuy n ti p ho c ng ưc l i mi nút cĩ th ch a m t ho c nhi u th () 19 Mng Petri Ví d t2 t1 p2 p1 t3 p4 p3 20 10
Mng Petri Mng Petri đưc đnh ngh ĩa b i s đ ánh d u các nút ca nĩ Vi c đánh d u các nút đưc ti n hành theo nguyên t c sau: mi chuy n ti p cĩ các nút vào và các nút ra nu t t c các nút vào c a m t chuy n ti p cĩ ít nh t mt th , thì chuy n ti p này là cĩ th vưt qua đưc, nu chuy n ti p này đưc th c hi n thì tt c các nút vào c a chuy n ti p s b ly đi m t th , và mt th sđưc thêm vào t t c các nút ra c a chuy n ti p nu 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 Mng 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 22 t4 11
Mng Petri Ví d t2 t2 khi t2 đưc v ưt qua 23 Mng Petri Ví d 24 12
Mng Petri Ví d 1: mơ t ho t đng c a đèn giao thơng red yr rg yellow gy 25 green Mng Petri Ví d 1: mơ t ho t đng c a 2 đ èn giao thơng red1 red2 yr1 yr2 rg1 yellow1 yellow2 rg2 gy1 gy2 26 green1 green2 13
Mng Petri Ví d 1: mơ t ho t đng an tồn c a 2 đ èn giao thơng red1 red2 safe yr1 yr2 rg1 yellow1 yellow2 rg2 gy1 gy2 27 green1 green2 Mng Petri Ví d 1: mơ t ho t đng an tồn và hp lý c a 2 đ èn giao thơng red1 red2 safe2 yr1 yr2 rg1 yellow1 rg2 yellow2 gy1 gy2 safe1 28 green1 green2 14
Mng Petri Ví d 2: mơ t chu k ỳ sng c a m t ng ưi tr con dy thì cưi thanh niên cĩ v cĩ ch ng ly hơn 29 ch t ch t Mng Petri Ví d 3: vi t th ư vàđc th ư begin receive_mail mail_box rest 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
Mng Petri Ví d 4: tình hu ng ngh n (dead-lock) P1 P2 P3 t1 t2 P4 P5 t3 t4 P7 P6 t5 t6 P8 P9 2 2 t7 t8 31 Mng Petri Ví d 4: gi i pháp ch ng ngh n P1 P2 P3 t1 t2 P4 P5 t3 t4 2 2 P7 P6 t5 t6 P8 P9 2 2 t7 t8 32 16
Mng Petri Ví d 5 H th ng c n mơ t bao g m m t nhà sn xu t, m t nhà tiêu th và mt kho hàng ch ch a đưc nhi u nh t 2 s n ph m Nhà sn xu t cĩ 2 tr ng thái • P1: khơng s n xu t • P2: đangsn xu t Nhà tiêu th cĩ 2 tr ng thái • C1: cĩ sn ph m đ tiêu th • C2: khơng cĩ sn 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 Mng Petri Ví d 5: mơ t tách r i m i thành ph n Sn xu t Ly t kho P1 P2 C1 C2 Gi vào kho Tiêu th Gi vào kho Gi vào kho 0 1 2 Ly t kho Ly t kho 34 17
Mng Petri Ví d 5: mơ t kt h p các thành ph n Sn xu t P1 Gi vào kho P2 Gi vào kho Ly t kho 2 0 1 Ly t kho C1 C2 Tiêu th 35 ðiu 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 dng ngơn ng phi hình th c, hình th c ho c ngơn ng lp trình đđc t các điu ki n 36 18
ðiu 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 ca 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 ðiu ki n tr ưc và sau Bài t p: đc t các hàm 1. Sp x p m t danh sách các s nguyên 2. ðo ng ưc các ph n t ca 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 đĩ mt mc tr u t ưng đc l p v i cách cài đt d li u b i ngơn ng lp trình ðc t mt 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 dng • 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 : →→→ Boolean false : →→→ Boolean ¬¬¬ _ :Boolean →→→ Boolean _ ∧∧∧ _ : Boolean x Boolean →→→ Boolean _ ∨∨∨ _ : Boolean x Boolean →→→ Boolean mt thao tác khơng cĩ tham s là mt h ng s mt giá tr ca ki u tr u t ưng đnh ngh ĩa đưc bi u di n b i kí t “_” 40 20
Ki u tr u t ưng Ví d 2: đc t ki u tr u t ưng Vector sort Boolean operations true : →→→ Boolean false : →→→ Boolean ¬¬¬ _ :Boolean →→→ Boolean _ ∧∧∧ _ : Boolean x Boolean →→→ Boolean _ ∨∨∨ _ : Boolean x Boolean →→→ Boolean mt thao tác khơng cĩ tham s là mt h ng s mt giá tr ca ki u tr u t ưng đnh ngh ĩa đưc bi u di n b i kí t “_” 41 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 vect : Integer x Integer →→→ Vector init : Vector x Integer →→→ Boolean ith : Vector x Integer →→→ Element change-ith : Vector x Integer x Element →→→ Vector supborder : Vector →→→ Integer infborder : Vector →→→ Integer 42 21
Ki u tr u t ưng Ví d 2: đc t ki u tr u t ưng Vector các thao tác trên ki u ch đưc đnh ngh ĩa mà khơng ch ra ng ngh ĩa c a nĩ • tc là ý ngh ĩa c a thao tác s dng các tiên đđđnh ngh ĩa ng ngh ĩa c a các thao tác • dùng t khĩa axioms đnh ngh ĩa các ràng bu c mà mt thao tác đưc đnh ngh ĩa • dùng t khĩa precondition 43 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 ≤≤≤ supborder (v) &&& infborder (v) ≤≤≤ j ≤≤≤ supborder (v) &&& i ≠≠≠ j ⇒⇒⇒ ith (change-ith (v, i, e), j) = ith (v, j) init (vect (i, j), k) = false infborder (v) ≤≤≤ i ≤≤≤ supborder (v) ⇒⇒⇒ init (change-ith (v, i, e), i) = true infborder (v) ≤≤≤ i ≤≤≤ supborder (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 44 22
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 tp h p 45 23