Model Checking LTL dengan NuSMV

Model Checking LTL dengan NuSMV Kuliah (Pengantar) Metode Formal Semester Ganjil 2015-2016 M. Arzaki Fakultas Informatika Telkom University FIF Tel-U

Desember 2015

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

1 / 23

Acknowledgements

Slide ini disusun berdasarkan materi yang terdapat pada sumber-sumber berikut: Buku: 1

2 3

Logic in Computer Science: Modelling and Reasoning about Systems, Edisi 2, 2004, oleh M. Huth dan M. Ryan (acuan utama). NuSMV 2.5 tutorial dari http://nusmv.fbk.eu/dan [email protected]. NuSMV 2.5 user manual dari http://nusmv.fbk.eu/dan [email protected].

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

2 / 23

Slide kuliah: 1

Slide kuliah Model Checking di University of Waikato oleh Robi Malik.

2

Slide kuliah Introduction to SMV di Software Engineering Lab, CMU, oleh Arie Gur…nkel.

3

Slide kuliah Model Cheking with NuSMV di University of Edinburgh oleh Paul Jackson.

4

Slide kuliah A Hands-on Tutorial on Model Checking – NuSMV – di Universitas Trento oleh A. Cimmati, M. Pistore, dan M. Roveri.

5

Slide kuliah NuSMV: A Simple Introduction di UCL oleh F. Raimondi.

6

Slide kuliah The NuSMV Model Chekcer di IIT Delhi oleh M. Pistore dan M. Roveri.

7

Slide kuliah Metode Formal di Free University of Bolzano oleh Alessandro Artale.

8

Slide kuliah Introduction to Computational Logic di Academia Sinica oleh Bow-Yaw Wang.

Beberapa gambar dapat diambil dari sumber-sumber di atas. Slide ini ditujukan untuk keperluan akademis di lingkungan FIF Telkom University. Jika Anda memiliki saran/ pendapat/ pertanyaan terkait materi dalam slide ini, silakan kirim email ke @telkomuniversity.ac.id. MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

3 / 23

Acknowledgements - Stackover‡ow

Penulis mengucapkan terima kasih kepada diskusi konstuktif pada forum Stackoverflow, terutama kepada Dejvuth Suwimonteerabuth dari TU München yang telah memberikan solusi untuk membuat kode NuSMV yang sederhana dan reliable.

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

4 / 23

Bahasan

1

Pemeriksaan Model dengan NuSMV: Motivasi

2

Beberapa Contoh Skrip NuSMV untuk Model LTL Sederhana

3

Latihan

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

5 / 23

Bahasan

1


2


3

Latihan

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

6 / 23


Kita sebelumnya telah melihat bagaimana cara memeriksa konsistensi dari suatu spesi…kasi sistem yang diformalisasi dengan logika proposisi menggunakan NuSMV. NuSMV selanjutnya akan digunakan untuk memeriksa apakah suatu formula LTL terpeneuhi pada suatu model atau tidak. Pemeriksaan dengan NuSMV akan mengurangi kesalahan yang mungkin terjadi dalam veri…kasi sistem yang dilakukan secara manual.

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

7 / 23

Bahasan

1


2


3

Latihan

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

8 / 23

Model LTL yang Ditinjau

Misalkan M = (S; !; L) adalah model LTL yang diilustrasikan dalam gambar berikut.

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

9 / 23

Skrip NuSMV untuk Model yang Ditinjau --LTL-model MODULE main VAR state : {s0,s1,s2}; -- himpunan state adalah ASSIGN init(state) := s0; next(state) := case state = s0 : state = s1 : state = s2 : esac; -- relasi transisi antar

MZI (FIF Tel-U)

{s0,s1,s2}

{s1,s2}; {s0,s2}; {s2}; state

Model Cheking LTL

Desember 2015

10 / 23

DEFINE p := state = s0; q := state = s0 j state = s1; r := state = s1 j state = s2; -- p, q, r diperlakukan sebagai label -- p benar di s0 saja -- q benar di s0 dan s1 -- r benar di s1 dan s2

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

11 / 23

LTLSPEC p & q; LTLSPEC ! r; LTLSPEC TRUE; LTLSPEC X r; LTLSPEC X (q & r);

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

12 / 23

LTLSPEC G !(p&r); LTLSPEC G (F r) ; LTLSPEC G (F p) -> G (F r); LTLSPEC G (F r) -> G (F p); LTLSPEC p U r;

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

13 / 23

Keluaran yang Dihasilkan NuSMV

– speci…cation (p & q) is true – speci…cation !r is true ******** WARNING ******** The initial states set of the …nite state machine is empty. This might make results of model checking not trustable. ******** END WARNING ******** – speci…cation TRUE is true – speci…cation X r is true

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

14 / 23

– speci…cation X (q & r) is false – as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample -> State: 1.1 <state = s0 r = FALSE q = TRUE p = TRUE – Loop starts here -> State: 1.2 <state = s2 r = TRUE q = FALSE p = FALSE -> State: 1.3 <– speci…cation G !(p & r) is true – speci…cation G ( F r) is true

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

15 / 23

– speci…cation ( G ( F p) -> G ( F r)) is true – speci…cation ( G ( F r) -> G ( F p)) is false – as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample -> State: 2.1 <state = s0 r = FALSE q = TRUE p = TRUE -> State: 2.2 <state = s1 r = TRUE p = FALSE – Loop starts here -> State: 2.3 <state = s2 q = FALSE -> State: 2.4 <– speci…cation (p U r) is true MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

16 / 23

Catatan

NuSMV tidak secara khusus dikembangkan untuk kepentingan komersial, oleh karenanya mungkin terdapat beberapa bug yang dapat muncul pada NuSMV. Bug dapat terjadi karena: I

I

skrip NuSMV yang dibuat tidak benar-benar merepresentasikan model LTL yang dimaksud algoritma model-checking pada NuSMV mengalami kesalahan

Untuk mempelajari NuSMV lebih jauh, silakan kirim email ke [email protected] atau [email protected] Pertanyaan terkait NuSMV juga dapat didiskusikan di Stackoverflow.

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

17 / 23

Cara Membaca Counterexample – speci…cation X (q & r) is false – as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample -> State: 1.1 <state = s0 r = FALSE q = TRUE p = TRUE – Loop starts here -> State: 1.2 <state = s2 r = TRUE q = FALSE p = FALSE -> State: 1.3 <-

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

18 / 23

Hal tersebut berarti M; s0 6j= X (q ^ r) karena X (q ^ r) tidak dipenuhi pada lintasan = s0 ! s2 (mulai loop di s2 ) atau lintasan = s0 ! s2 ! s2 ! .

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

19 / 23

– speci…cation ( G ( F r) -> G ( F p)) is false – as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample -> State: 2.1 <state = s0 r = FALSE q = TRUE p = TRUE -> State: 2.2 <state = s1 r = TRUE p = FALSE – Loop starts here -> State: 2.3 <state = s2 q = FALSE -> State: 2.4 <-

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

20 / 23

Hal tersebut berarti M; s0 6j= GF (r) ! GF (p) karena GF (r) ! GF (p) tidak dipenuhi pada lintasan = s0 ! s1 ! s2 (mulai loop di s2 ) atau lintasan = s0 ! s1 ! s2 ! s2 ! .

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

21 / 23

Bahasan

1


2


3

Latihan

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

22 / 23

Latihan

Latihan Buatlah skrip NuSMV yang memodelkan suatu lampu lalu lintas sederhana, kemudian periksa apakah model tersebut memenuhi spesi…kasi formal yang diberikan.

MZI (FIF Tel-U)

Model Cheking LTL

Desember 2015

23 / 23

Model Checking LTL dengan NuSMV

Recommend Documents