Pengenalan Dasar Model Checker NuSMV

Pengenalan Dasar Model Checker NuSMV Kuliah (Pengantar) Metode Formal Semester Ganjil 2015-2016 M. Arzaki Fakultas Informatika Telkom University FIF Tel-U

Oktober 2015

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

1 / 30

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 Checker NuSMV

Oktober 2015

2 / 30

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 Checker NuSMV

Oktober 2015

3 / 30

Bahasan

1

Apa Itu NuSMV

2

Instalasi dan Cara Memakai NuSMV

3

Sintaks Dasar NuSMV

4

Pemakaian NuSMV terkait Logika Proposisi

5

NuSMV untuk Konsistensi Spesi…kasi Sistem

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

4 / 30

Bahasan

1

Apa Itu NuSMV

2


3

Sintaks Dasar NuSMV

4


5


MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

5 / 30

Apa Itu NuSMV? SMV: Symbolic Model Veri…er NuSMV: New Symbolic Model Veri…er NuSMV atau SMV merupakan sebuah alat bantu (tools) yang menyediakan suatu bahasa untuk mendeskripsikan suatu model sistem yang dijelaskan dalam LTL (Linear Time Temporal Logic) maupun CTL (Computation Tree Logic). NuSMV merupakan suatu model checker (alat untuk memeriksa suatu model). SMV awalnya dikembangkan oleh K. L. McMillan dan E. M. Clarke di CMU. Saat ini NuSMV dikembangkan sebagai joint project dari: FBK-IRST, CMU, University of Genova, dan University of Trento. NuSMV merupakan suatu produk open source. Untuk mengetahui lebih lanjut tentang NuSMV, silakan lihat di http://nusmv.fbk.eu/.

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

6 / 30

Bahasan

1

Apa Itu NuSMV

2


3

Sintaks Dasar NuSMV

4


5


MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

7 / 30

Instalasi NuSMV pada Windows File yang diperlukan untuk instalasi NuSMV pada sistem operasi Windows maupun Linux dapat diunduh di http://nusmv.fbk.eu/. File yang diperlukan juga sudah di-share pada forum diskusi di idea. Silakan hapus ekstensi .pdf pada …le NuSMV.zip.pdf dan lakukan ekstraksi pada …le tersebut. Instalasi pada Windows dapat dilakukan dengan megikuti langkah-langkah berikut: 1

Lakukan klik ganda (double click) NuSMV-2.5.4-i386-pc-mingw32.exe.

2

Ikuti langkah-langkah instalasi sesuai petunjuk. Usahakan agar path folder instalasi tidak mengandung spasi dan karakter non alfanumerik seperti , !, @, #, $, ^, &, *, (, ). Sebagai contoh, instalasi dapat dilakukan pada path C:nNuSMV.

3

NuSMV siap digunakan.

Instalasi telah berhasil dilakukan pada sistem operasi Windows Vista-32 bit dan Windows 7-64 bit.

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

8 / 30

Catatan Agar eksekusi …le .smv dapat dilakukan tanpa mengkopi …le tersebut ke direktori bin (contohnya C:nNuSMVn2.5.4nbin), Anda dapat memodi…kasi path dan environment variable yang ada pada Windows. Pada environment variable, tambahkan variable dengan nama path dengan value direktori bin (contohnya C:nNuSMVn2.5.4nbin).

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

9 / 30

Instalasi NuSMV pada Linux

Instalasi NuSMV pada Linux dapat dilakukan dengan cara-cara berikut: 1

Lakukan ekstraksi pada …le NuSMV-2.5.4.tar.gz.

2

Pindahkan folder hasil ekstraksi ke direktori yang tidak memakai spasi. Contohnya: /Documents/NuSMV-2.5.4. NuSMV siap digunakan.

3

Instalasi telah berhasil dilakukan pada sistem operasi Linux Ubuntu 14.04 (TLS).

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

10 / 30

Program Pertama Silakan ketik teks berikut pada teks editor favorit Anda. Gunakan spasi atau tab untuk indensasi. --Example-01 MODULE main VAR p : boolean; q : boolean; phi1: boolean; phi2: boolean; ASSIGN phi1 := !p & q; phi2 := p -> p j q; LTLSPEC phi1 LTLSPEC phi2

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

11 / 30

Simpan program yang telah Anda buat dengan nama example-01.smv pada folder bin, contohnya: C:nNuSMVn2.5.4nbin (pada Windows) /Documents/NuSMV-2.5.4/ NuSMV-2.5.4-x86_64-unknown-linux-gnu/bin (pada Linux) Jika path dan environment variable sudah ditambahkan pada Windows, maka program example-01.smv dapat disimpan pada folder apapun selain bin. Selanjutnya eksekusi perintah berikut:

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

12 / 30

Pada Windows: 1

2

Gunakan command prompt (ketikkan cmd pada launcher ). Masuk ke direktori C:nNuSMVn2.5.4nbin. Hal ini dapat dilakukan dengan perintah cd. Ketik C:nNuSMVn2.5.4nbin>NuSMV.exe example-01.smv. Jika path dan environment variable sudah ditambahkan, Anda dapat menjalankan program di direktori apapun, contohnya D:nMyProgramnNuSMVnNuSMV example-01.smv.

Pada Linux: 1

Gunakan terminal (ketikkan terminal pada launcher ). Masuk ke direktori bin, contohnya arzaki@arzaki-ThinkPad-E455: /Documents/NuSMV-2.5.4/ NuSMV-2.5.4-x86_64-unknown-linux-gnu/bin.

2

Tambahkan perintah ./NuSMV example-01.smv.

Jika eksekusi program lancar, maka command prompt/ terminal akan memberikan keluaran berikut:

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

13 / 30

*** *** *** *** *** *** *** *** *** *** ***

This is NuSMV 2.5.4 (compiled on Fri Oct 28 13:47:30 UTC 2011) Enabled addons are: compass For more information on NuSMV see or email to . Please report bugs to Copyright (c) 2010, Fondazione Bruno Kessler This version of NuSMV is linked to the CUDD library version 2.4.1 Copyright (c) 1995-2004, Regents of the University of Colorado This version of NuSMV is linked to the MiniSat SAT solver. See http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

14 / 30

– speci…cation phi1 is false – as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample – Loop starts here -> State: 1.1
State: 1.2 <– speci…cation phi2 is true

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

15 / 30

Bahasan

1

Apa Itu NuSMV

2


3

Sintaks Dasar NuSMV

4


5


MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

16 / 30

Sintaks Dasar NuSMV Perhatikan kembali program yang sebelumnya telah dibuat. --Example-01 MODULE main VAR p : boolean; q : boolean; phi1: boolean; phi2: boolean; ASSIGN phi1 := !p & q; phi2 := p -> p j q; LTLSPEC phi1 LTLSPEC phi2

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

17 / 30

Struktur program adalah --Example-01 (nama program yang bersifat opsional, komentar selalu didahului dengan karakter “--”) MODULE main (nama modul). VAR (deklarasi variabel). ASSIGN (assignment, contohnya untuk membuat proposisi majemuk). LTLSPEC (pemeriksaan spesi…kasi sistem dalam formula logika tertentu) LTLSPEC dapat diganti dengan SPEC saja atau CTLSPEC. Jika diganti dengan SPEC, maka hasilnya akan sama dengan jika kita memakai CTLSPEC.

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

18 / 30

Tipe Data Tipe data pada NuSMV ada beberapa macam, yaitu: boolean: system_ok : boolean; enumeration: state : {ready, busy, waiting, stopped}; bounded integers: num : 1..8; array and bit vectors: arr : array 0..3 of {red,yellow,green}; bv: signed word[8];

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

19 / 30

Assignment immediate assignment: ASSIGN x := <expression>; atau DEFINE x := <expression>; initialization: ASSIGN init(x) := <expression>; progression: ASSIGN next (x) := <expression>;

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

20 / 30

Operator Logika Proposisi Operator logika proposisi yang dipakai pada NuSMV adalah: Simbol : ^ _ ! $

Operator pada NuSMV ! & j -> <->

Sebagai contoh, formula p ! q ^ r dan p $ p _ :q pada NuSMV berturut-turut dapat ditulis sebagai: p -> q & r p <-> p j !q

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

21 / 30

Bahasan

1

Apa Itu NuSMV

2


3

Sintaks Dasar NuSMV

4


5


MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

22 / 30

Cara Kerja NuSMV Secara umum NuSMV bekerja dengan cara memeriksa model yang dimasukkan oleh pengguna. Jika model tersebut salah (false), maka NuSMV akan memberikan suatu counterexample yang menjelaskan kesalahan model tersebut. Lihat kembali keluaran yang diberikan NuSMV untuk masukan program example-01.smv. – speci…cation phi1 is false – as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample – Loop starts here -> State: 1.1
State: 1.2 <– speci…cation phi2 is true

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

23 / 30

Pada example-01.smv, program NuSMV dibuat untuk memeriksa kebenaran formula 1 :=

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

24 / 30

Pada example-01.smv, program NuSMV dibuat untuk memeriksa kebenaran formula 1 := :p ^ q dan 2 :=

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

24 / 30

Pada example-01.smv, program NuSMV dibuat untuk memeriksa kebenaran formula 1 := :p ^ q dan 2 := p ! p _ q.

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

24 / 30

Pada example-01.smv, program NuSMV dibuat untuk memeriksa kebenaran formula 1 := :p ^ q dan 2 := p ! p _ q. NuSMV memberikan keluaran bahwa spesi…kasi (formula) 1 dapat salah ketika I (p) = T dan I (q) = F. Untuk spesi…kasi 2 ,

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

24 / 30

Pada example-01.smv, program NuSMV dibuat untuk memeriksa kebenaran formula 1 := :p ^ q dan 2 := p ! p _ q. NuSMV memberikan keluaran bahwa spesi…kasi (formula) 1 dapat salah ketika I (p) = T dan I (q) = F. Untuk spesi…kasi 2 , NuSMV menyatakan bahwa 2 adalah spesi…kasi (formula) yang benar (tidak pernah salah). Jelas bahwa 2 adalah suatu tautologi (bersifat absah/ valid). Dari observasi terhadap keluaran program ini, kita dapat melihat bahwa NuSMV dapat digunakan untuk memeriksa falsi…ability dari suatu formula logika proposisi . Lebih jauh kita memiliki: Untuk setiap masukan yang berupa formula logika proposisi , maka NuSMV akan mengeluarkan keluaran berikut:

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

24 / 30

Pada example-01.smv, program NuSMV dibuat untuk memeriksa kebenaran formula 1 := :p ^ q dan 2 := p ! p _ q. NuSMV memberikan keluaran bahwa spesi…kasi (formula) 1 dapat salah ketika I (p) = T dan I (q) = F. Untuk spesi…kasi 2 , NuSMV menyatakan bahwa 2 adalah spesi…kasi (formula) yang benar (tidak pernah salah). Jelas bahwa 2 adalah suatu tautologi (bersifat absah/ valid). Dari observasi terhadap keluaran program ini, kita dapat melihat bahwa NuSMV dapat digunakan untuk memeriksa falsi…ability dari suatu formula logika proposisi . Lebih jauh kita memiliki: Untuk setiap masukan yang berupa formula logika proposisi , maka NuSMV akan mengeluarkan keluaran berikut: counterexample berupa interpretasi untuk setiap variabel proposisi atom yang membuat I ( ) = F apabila merupakan formula yang falsi…able,

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

24 / 30

Pada example-01.smv, program NuSMV dibuat untuk memeriksa kebenaran formula 1 := :p ^ q dan 2 := p ! p _ q. NuSMV memberikan keluaran bahwa spesi…kasi (formula) 1 dapat salah ketika I (p) = T dan I (q) = F. Untuk spesi…kasi 2 , NuSMV menyatakan bahwa 2 adalah spesi…kasi (formula) yang benar (tidak pernah salah). Jelas bahwa 2 adalah suatu tautologi (bersifat absah/ valid). Dari observasi terhadap keluaran program ini, kita dapat melihat bahwa NuSMV dapat digunakan untuk memeriksa falsi…ability dari suatu formula logika proposisi . Lebih jauh kita memiliki: Untuk setiap masukan yang berupa formula logika proposisi , maka NuSMV akan mengeluarkan keluaran berikut: counterexample berupa interpretasi untuk setiap variabel proposisi atom yang membuat I ( ) = F apabila merupakan formula yang falsi…able, pernyataan bahwa “speci…cation formula yang falsi…able.

MZI (FIF Tel-U)

is true” apabila

Model Checker NuSMV

bukan merupakan

Oktober 2015

24 / 30

Memeriksa Satis…ability dengan NuSMV Permasalahan Diberikan formula logika proposisi , apakah kita dapat memeriksa keterpenuhan (satis…ability ) dari ? Jika ya, bagaimana caranya? Untuk mengetahui jawaban dari permasalahan, terlebih dulu eksekusi program .smv berikut.

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

25 / 30

Memeriksa Satis…ability dengan NuSMV Permasalahan Diberikan formula logika proposisi , apakah kita dapat memeriksa keterpenuhan (satis…ability ) dari ? Jika ya, bagaimana caranya? Untuk mengetahui jawaban dari permasalahan, terlebih dulu eksekusi program .smv berikut. --Example-02 MODULE main VAR p : boolean; q : boolean; r : boolean; s : boolean; phi1: boolean; phi2: boolean; phi3: boolean;

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

25 / 30

ASSIGN phi1 := (p j q) & (! q j r) & (! phi2 := (p j q j r j s); phi3 := !(p j q j r js); LTLSPEC phi1 LTLSPEC phi2 LTLSPEC phi3

MZI (FIF Tel-U)

r j s) -> p j s;

Model Checker NuSMV

Oktober 2015

26 / 30

NuSMV akan memberikan keluaran berikut: – speci…cation phi1 is true – speci…cation phi2 is false – as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample – Loop starts here -> State: 1.1

MZI (FIF Tel-U)

-> State: 1.2 <– speci…cation phi3 is false – as demonstrated by the following execution sequence Trace Description: LTL Counterexample Trace Type: Counterexample – Loop starts here -> State: 2.1
State: 2.2 <-

Model Checker NuSMV

Oktober 2015

27 / 30

Untuk memeriksa apakah teorema berikut.

bersifat terpenuhi atau tidak kita dapat memakai

Teorema

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

28 / 30



Teorema Formula logika proposisi tersalahkan (falsi…able).

terpenuhi (satis…able) jika dan hanya jika :

Sebagai contoh, pada program example-02 smv sebelumnya, untuk memeriksa apakah p _ q _ r _ s bersifat satis…able maka kita dapat melakukannya dengan memeriksa apakah : (p _ q _ r _ s) bersifat falsi…able.

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

28 / 30





Sebagai contoh, pada program example-02 smv sebelumnya, untuk memeriksa apakah p _ q _ r _ s bersifat satis…able maka kita dapat melakukannya dengan memeriksa apakah : (p _ q _ r _ s) bersifat falsi…able. Kita melihat bahwa NuSMV meyatakan bahwa : (p _ q _ r _ s) bersifat falsi…able dengan counterexample berikut:

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

28 / 30





Sebagai contoh, pada program example-02 smv sebelumnya, untuk memeriksa apakah p _ q _ r _ s bersifat satis…able maka kita dapat melakukannya dengan memeriksa apakah : (p _ q _ r _ s) bersifat falsi…able. Kita melihat bahwa NuSMV meyatakan bahwa : (p _ q _ r _ s) bersifat falsi…able dengan counterexample berikut:I (p) = T, I (q) = F, I (r) = F, dan I (s) = F. Jelas bahwa hal ini berakibat I (: (p _ q _ r _ s)) = F, sehingga I ( ) = I (p _ q _ r _ s) = T.

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

28 / 30

Bahasan

1

Apa Itu NuSMV

2


3

Sintaks Dasar NuSMV

4


5


MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

29 / 30

Latihan Buatlah NuSMV untuk memecahkan masalah-masalah berikut. 1

Periksa apakah spesi…kasi sistem berikut konsisten atau tidak dengan memakai NuSMV: (1) ketika system software di-upgrade, user tidak dapat mengakses …le system; (2) jika user dapat mengakses …le system, maka user dapat menyimpan …le baru; (3) jika user tidak dapat menyimpan …le baru, maka system software tidak sedang di-upgrade.

2

Periksa apakah koleksi formula A = f:p ! q; :p $ r; :q $ s; :p ! sg konsisten atau tidak.

3

Pecahkan masalah perampokan bank yang dijelaskan pada slide kuliah 3.LogikaProposisi-3.pdf dengan NuSMV.

MZI (FIF Tel-U)

Model Checker NuSMV

Oktober 2015

30 / 30

Pengenalan Dasar Model Checker NuSMV

Recommend Documents