TAILIEUCHUNG - PROMELA & SPIN

Dalam PROMELA tidak ada perbedaan antara conditions dan statements. Eksekusi dari statement bergantung kepada sifat executability nya. PROMELA statement bisa executable atau blocked bergantung kepada nilai dari variable atau isi dari message channels. Jika kondisi benar (holds) maka statement dieksekusi. Jika tidak, maka dia akan terblokir (blocked) sampai condition holds | PROMELA & SPIN Budi Rahardjo Kuliah Metoda Formal 2004 PROMELA & SPIN - Budi Rahardjo PROMELA & SPIN PROMELA = PROcess MEta Language Sebuah bahasa untuk men-spesifikasi-kan sistem Menggabungkan CSP, C, SDL SPIN merupakan tools untuk melakukan (model) checking terhadap sistem yang dituliskan dalam PROMELA Bahasa PROMELA PROMELA & SPIN - Budi Rahardjo OBJECTS Ada 3 objects (akan dijelaskan nanti) Processes Message channels State variables Object ini bisa ditransalasikan menjadi finite state machine PROMELA & SPIN - Budi Rahardjo Executability of statements Dalam PROMELA tidak ada perbedaan antara conditions dan statements Eksekusi dari statement bergantung kepada sifat executability nya PROMELA statement bisa executable atau blocked bergantung kepada nilai dari variable atau isi dari message channels Jika kondisi benar (holds) maka statement dieksekusi. Jika tidak, maka dia akan terblokir (blocked) sampai condition holds PROMELA & SPIN - Budi Rahardjo Variabel & Data Types Ada 6 predefined data types Bit, bool, byte, short, int, chan Ukuran (1), (1), (8), (16), (32) bit, kecuali channel Chan -> message channel, yaitu sebuah object yang dapat menyimpan beberapa nilai yang disatukan menjadi sebuah struktur Contoh penggunaan bool flag; int state; byte msg; PROMELA & SPIN - Budi Rahardjo Array Variabel dapat dinyatakan sebagai array byte state[N] state[0] = state[3] + 5 * state[3*2/n] Declaration dan assigments selalu executable PROMELA & SPIN - Budi Rahardjo Process proctype A() { byte state; state = 3} merupakan deklarasi sebuah proses dengan sebuah variable yang bernama state Tanda titik koma (semicolon) merupakan statement separator (bukan statement terminator). Ada dua statement separator: anak panah -> dan titik koma ;. Keduanya ekivalen PROMELA & SPIN - Budi Rahardjo Contoh byte state = 2; proctype A() { (state == 1) -> state = 3} proctype B() { state = state – 1} PROMELA & SPIN - Budi Rahardjo Initial Process init { run A(); run .

• Quản trị mạng
• Message channels
• Control Flow
• Case selection
• Initial Process
• Data Types
• Executability of statements
• connection hardware
• communication channels
• receive data
• TCP protocol
• Case Diagram
• handle message