1 Pengantar Metoda Formal Budi Rahardjo 24 September 20052 23 Daftar Isi 1 Pendahuluan Latar Belakang Kecelakaan akibat software atau hardware Proses ...
A Laboratorium BDD 47 A.1 Masuk ke sistem UNIX . . . . . . . . . . . . . . . . . . . . . . 47 A.2 Mencoba BDD . . . . . . . . . . . . . . . . . . . . . . . . . . 48 A.3 Equivalency, isomorphism . . . . . . . . . . . . . . . . . . . . 49 A.4 Efek dari ordering . . . . . . . . . . . . . . . . . . . . . . . . 50 A.5 Lain-lain . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Informasi mengenai buku ini. c 2004,2005 Budi Rahardjo. Buku ini memiliki lisensi CreHak Cipta ° ative Commons 1 . Buku ini dapat digunakan untuk keperluan apa saja dan didistribusikan secara gratis.
1 Informasi mengenai http://crativecommons.org
Creative
Commons
dapat
dilihat
pada
situs
Bab 1
Pendahuluan Buku ini merupakan panduan kuliah Metoda Formal (dalam desain perangkat keras) atau Formal Methods for Hardware Design yang diberikan oleh Departemen (Jurusan) Teknik Elektro ITB. Buku ini merupakan kelanjutan dari technical report [12] yang merupakan hasil dari Riset Unggulan Terpadu (RUT) dan rangkuman dari beberapa makalah yang relevan dengan bidang metoda formal ini. 1 Beberapa bagian dari buku ini membutuhkan latar belakang matematika diskrit dan logic. Agar bisa berdiri sendiri, buku ini memberikan beberapa pengantar tentang matematika diskrit dan logic. Namun tentunya buku ini bukan buku utama untuk hal itu. Bagi anda yang tertarik dengan referensi yang lebih komplit silahkan gunakan buku Kenneth Rosen [13]. Demikian pula beberapa topik, seperti notasi formal yang ada pada bab Formal Specification, masing-masing dapat menjadi buku tersendiri. Memang pada kenyataannya banyak buku untuk masing-masing topik tersebut. Namun buku ini bermaksud mengambil bagian yang penting untuk sekedar memberikan wawasan kepada pembaca. Buku ini berisi beberapa contoh yang diperoleh dari kelas yang telah diajarkan oleh penulis. Beberapa contoh menggunakan tools yang dapat diperoleh secara gratis dan komersial. Ada tools yang menggunakan sistem UNIX. Untuk bagian itu diharapkan pembaca dapat mempelajari UNIX sendiri. 1
Buku ini masih dalam proses penulisan sehingga masih banyak bagian yang belum selesai. Proses penulisan menggunakan LATEXyang belum terkonfigurasi untuk bahasa Indonesia. Untuk itu anda akan menemukan beberapa kejanggalan pada pemenggalan kata.
5
6
BAB 1. PENDAHULUAN Tabel 1.1: Perkembangan kompleksitas software Sistem Operasi Tahun Jumlah Baris (lines of code) Windows 3.1 1992 3 juta Windows NT 1992 4 juta Windows 95 1995 15 juta Windows NT 4.0 1996 16,5 juta Windows 98 1998 18 juta Windows 2000 2002 35 s/d 60 juta
1.1
Latar Belakang “There are two ways of constructing a software design. One way is to make it so simple that there are obviously no deficiencies. And the other way is to make it so complicated that there are no obvious deficiencies.” (C.A.R. Hoare)
Apa itu metoda formal? Mengapa metoda formal dibutuhkan? Apa hubungannya dengan desain hardware? Bagian ini akan mencoba menjawab pertanyaan tersebut. Metoda formal pada mulanya muncul di dunia software (perangkat lunak)2 . Namun istilah metoda formal ini juga muncul di dunia hardware dan bahkan kelihatannya penerapan metoda formal lebih banyak suksesnya di bidang hardware dibandingkan dengan bidang software. Jika kita perhatikan tingkat kompleksitas dari desain software dan hardware, maka kita dapat melihat kenaikan yang cukup tajam. Bahkan trendnya menunjukkan tanda-tanda makin meningkat. Sebagai contoh, software wordprocessor Wordstar (WS) dahulu cukup dimasukkan ke dalam disket dalam ukuran 300 KBytes. Sementara ini, program Microsoft Word 2000 harus didistribusikan dalam CD-ROM yang ukurannya ratusan MBytes. Sebagai gambaran, tabel 1.1 menunjukkan perkembangan kompleksitas dari operating system Microsoft Windows. Kompleksitas dalam tabel tersebut ditunjukkan dengan banyaknya jumlah baris kode (lines of code (LOC)). Sebagai perkiraan, setiap KLOC dapat memiliki 5 sampai dengan 50 bugs. Jumlah transistor dalam sebuah Integrated Circuit (IC) sudah mencapai jutaan transistor. Pentium chip memiliki jutaan transistor. Kesemuannya 2
Banyak istilah asing yang dipaksakan diterjemahkan ke dalam bahasa Indonesia. Hasilnya justru malah membingungkan. Istilah software akan digunakan dalam buku ini agar tidak membingungkan.
1.1. LATAR BELAKANG
7
Tabel 1.2: Kompleksitas software lainnya [7] Sistem Jumlah Baris Kode Solaris 7 400.000 Linux 1,5 juta Boeing 777 7 juta Space Shuttle 10 juta Netscape 17 juta Space Station 40 juta Windows XP 40 juta
ini membutuhkan konsep desain yang berbeda dengan mendesain software atau hardware yang ukurannya kecil. Jika kompleksitas ini belum terbayang, maka anda dapat mencoba membayangkan tingkat kesulitan dalam mendesain rumah 1 tingkat dengan mendesain hotel 150 tingkat. Desain rumah 1 tingkat dapat anda percayakan kepada seorang sarjana yang baru saja lulus dari perguruan tinggi. Tapi, apakah anda akan mempercayakan desain hotel 150 tingkat kepada seorang mahasiswa yang baru lulus? Kemungkinan besar, tidak. Demikian pula, apakah metodologi desainnya akan sama? Mendesain rumah 1 tingkat bisa dilakukan dengan “coba-coba”, tapi mendesain hotel 150 tingkat tidak dapat dilakukan dengan cara coba-coba. Paradigma atau metoda desain yang baru dibutuhkan untuk menangani tingkat kompleksitas yang tinggi, khususnya untuk mengurangi jumlah kesalahan (bugs) dan mempercepat waktu yang dibutuhkan untuk mengembangkan dan memasarkan. Time to market di dunia yang high-tech ini sangat sempit. Khususnya untuk aplikasi yang membutuhkan keandalan tinggi (yang sering disebut mission critical applications), perhatian dalam desain dan pengujuan perlu mendapat perhatian yang lebih. Aplikasi yang membutuhkan ketelitian tinggi antara lain aplikasi untuk kesehatan (misalnya alat pacu jantung), sistem pengendali rudal nuklir atau pesawat ruang angkasa, pengendali pesawat terbang (fly-by-wire), dan masih banyak aplikasi sejenis lainnya. Ada beberapa masalah dalam desain dan pengujian sistem yang membutuhkan tingkat keandalan tinggi. Metoda formal membantu di bidang ini dengan penggunaan metoda matematik yang lebih rigorous.
8
BAB 1. PENDAHULUAN
1.2
Kecelakaan akibat software atau hardware
Untuk meyakinkan bahwa masalah ini bukan hanya masalah akademis saja, pada bagian ini akan didaftar beberapa contoh kasus kecelakaan yang disebabkan oleh adanya kesalahan (bugs) pada software dan/atau hardware. Akibat yang ditimbulkan oleh kesalahan ini bervariasi dari ketidak-nyamanan (inconvenience) sampai korban jiwa (fatal). 1. 22 Juli 1962. Roket pembawa Mariner I (yang akan digunakan untuk menjelajah ke Venus) terpaksa diledakkan. Penyebab utamanya adalah persamaan matematis yang digunakan untuk mengendalikan roket pembawa Mariner I kekurangan tanda “bar” (garis di atas simbol yang digunakan untuk menyatakan rata-rata atau average). Akibat kesalahan ini, komputer yang digunakan untuk mengendalikan roket menyatakan bahwa roket tak terkendali, meskipun sebetulnya roket tidak apa-apa. Akibatnya roket terpaksa harus dihancurkan untuk menghindari kecelakaan yang berakhibat lebih fatal. Sumber [15]. 2. 10 April 1981. The bug heard round the world. Pesawat ulang alik Columbia batal diluncurkan. Penyebabnya adalah hardware. Pada tanggal ini, pesawat ulang alik (space shuttle) Columbia batal diluncurkan 20 menit sebelum waktu yang sudah direncanakan. Penyebabnya adalah tidak sinkronnya clock komputer utama dan komputer backup. Untuk meningkatkan keandalan, komputer pengendali dari pesawat ulang alik tersebut terdiri dari empat (4) komputer utama dan sebuah komputer backup. Ternyata kadang-kadang (pobabilitasnya 1 dari 67) clock komputer utama (primary) lebih cepat satu cycle dari komputer backup ketika dihidupkan. Akibatnya komputer backup menunggu dan menunggu untuk sebuah sinyal yang tidak kunjung datang (deadlock). Peluncuran terpaksa dibatalkan. Sumber: [10]. 3. 25 Februari 1991. Di bidang militer, Patriot Amerika gagal menanggulangi roket scud milik Irak. Pada perang antara Irak dan Amerika ini, roket scud dari Irak menewaskan 28 tentara Amerika dan menciderai 98 tentara di barak dekat Dhahran, Saudi Arabia. Penyebabnya adalah kesalahan software. Patriot missile defense system menggunakan software untuk melakukan scanning ke angkasa dengan menggunakan radar (yang memiliki lebih dari 5000 elemen) sampai dia menemukan targetnya. Data radar yang diterima menunjukkan kecepatan dari target tersebut. Sistem Patriot kemudian menentukan arahnya.
1.2. KECELAKAAN AKIBAT SOFTWARE ATAU HARDWARE
9
Persamaan yang digunakan untuk melakukan tracking memiliki kesalahan 1/10 juta detik dalam setiap detiknya. Kesalahan ini dapat terakumulasi dan menjadi besar. US Army membuat prosedur baku bahwa mesin harus direset secara berkala untuk menghilangkan akumulasi kesalahan tersebut. Diperkirakan sistem Patriot hanya dapat digunakan secara maksimal selama 14 jam berturut-turut. Pada waktu kejadian, sistem Patriot sudah digunakan selama 5 hari berturutturut sehingga timingnya sudah bergeser sebesar 36/100 detik (sudah cukup besar). Kesalahan ini sebetulnya sudah diketahui, akan tetapi perbaikan (upgrade) yang dikerjakan di Ft. McGuire Air Force base membutuhkan waktu untuk mencapai tujuan dengan cara diterbangkan ke Riyadh, kemudian dikirimkan melalui truk ke Dhahran, dan akhirnya dipasang di tempat instalasi Patriot. Ternyata sudah terlambat. Sumber [15]. 4. 4 Juni-Juli 1991. Di bidang telekomunikasi, telepon di daerah Los Angles, San Francisco, Washington DC, West Virginia, Baltimore, Greensboro terputus. Penyebabnya adalah kesalahan software. Software yang digunakan untuk mengatur telephone switching dibuat oleh perusahaan DSC Communications. Software ini terdiri atas jutaan baris. Program sudah diuji selama 13 minggu dan sudah berjalan dengan sempurna. Kemudian sebelum instalasi mereka “memperbaiki” 3 baris kode saja dan merasa tidak perlu diuji kembali (karena akan menghabiskan 13 minggu lagi). Akibat “perbaikan” ini sistem justru menjadi crash. Sumber [15]. 5. 4 Juni 1996. Roket Ariane 5 meledak 40 detik setelah diluncurkan. Sumber informasi: European Space Agency (www.esa.int). 6. Radar dari HMS Sheffield salah mengidentifikasi roket Exocet milik Argentina sebagai roket non-Soviet sehingga diangap sebagai kawan. Tidak ada alarm yang dinyalakan. Akibatnya kapal tersebut tenggelam beserta awak kapalnya. Kelalaian ini disebabkan oleh design errors. Sumber informasi: ACM Software Engineering Notes 8 (3). 7. Juni 2004. Air traffic controller di Inggris (West Drayton control center) bermasalah (down) karena adanya “upgrade”. Penerbangan terpaksa diundurkan (delay) sehingga menyebabkan ketidaknyamanan penumpang. Tidak ada korban dan tidak ada informasi yang lebih lanjut mengenai masalah “update” tersebut.
10
BAB 1. PENDAHULUAN Sumber berita: http://news.bbc.co.uk/1/hi/uk/3772663.stm http://www.nats.co.uk/news/news stories/2004 06 03.html 8. Tanggal tidak diketahui. NASA Mars Lander menabrak permukaan Mars. Kesalahan terjadi karena ada perbedaan satuan ukuran yang digunakan, yaitu antara Inggris dan metric unit. Akibatnya, trayektori dari Mars Lander tersebut menjadi salah. Sang Lander mematikan mesinnya terlalu dini sehingga terjadi crash. Kerugian diperkirakan 165 juta dolar. 9. Tanggal tidak diketahui. Denver International Airport mengimplementasikan sistem penanganan bagasi secara otomatis, dengan menggunakan jalur-jalur (track) yang semuanya dikendalikan dengan software. Pada saat pengujian ternyata kereta bagasi tidak dapat mendeteksi kesalahan dan tidak dapat kembali (recover) dari error. Kereta yang kosong tidak diisi. Sementara itu kereta yang sudah berisi bagasi diisi lagi sehingga melebihi beban. Penyebabnya juga software. Akhirnya pengoperasian sistem ini terlambat 11 bulan dan mengakibatkan kerugian 1 juta dolar seharinya.
10. Tanggal tidak diketahui. MV-22 Osprey merupakan sebuah pesawat militer yang menggabungkan helikopter (yang dapat bergerak vertikal) dan pesawat terbang biasa. Tingkat kompleksitas dari aerodinamik dari pesawat ini sangat kompleks sehingga dibutuhkan software canggih untuk mengendalikannya. Pesawat ini juga menggunakan sistem redundan untuk meningkatkan keandalannya. Namun pada suatu saat terjadi kerusakan pada sistem hydraulic. Ini memang masalah serius, namun biasanya bisa dikendalikan. Sanganya pada saat masalah ini terjadi, sistem backup tidak berjalan sebagaimana mestinya. Pesawat jatuh dan empat orang marine mati. 11. 1988. US Vicennes. Di tahun 1988, sebuah kapal laut Amerika menembakkan peluru kendali dan menjatuhkan sebuah pesawat yang diidentifikasi sebagai musuh. Ternyata pesawat yang ditembak adalah sebuah pesawat komersial Airbus A320 yang sangat jauh berbeda dengan pesawat musuh. Akibatnya 290 penumpang pesawat tersebut tewas. Angkatan laut Amerika menyalahkan sistem penjejak (tracking software) yang memperagakan output yang tidak dapat dimengerti (cryptic) sehingga mengambil kesimpulan yang salah. Selain kasus-kasus di atas, sebetulnya masih banyak kecelakaan lain yang terjadi di dunia engineering yang tidak terkait dengan hardware atau soft-
1.3. PROSES PENGEMBANGAN HARDWARE / SOFTWARE
11
Specification Validation
Verification User Automatic synthesis
Validation
Implementation #1
Translation
Manual synthesis
Implementation #2
Translation
Implementation n
Gambar 1.1: Diagram proses pengembangan ware. Buku Henry Petroski [11] menceritakan beberapa kesalahan dalam desain jembatan dan bangunan yang berakibat fatal. European Space Agency (ESA) memiliki situs web (www.esa.int) yang memberitakan berbagai masalah tentang penerbangan ruang angkasa. Usenet newsgroup comp.risk juga banyak menceritakan kecelakaan yang diakibatkan oleh salah desain.
1.3
Proses Pengembangan Hardware / Software
Secara umum, proses pengembangan (development) perangkat keras atau perangkat lunak meliputi beberapa tahap; spesifikasi (specification), implementasi (implementation), dan validasi (validation) serta verifikasi (verification). 3 Kegiatan lain yang terkait dengan tahapan tersebut antara lain adalah automated systhesis dan translation. Kerangka tahapan tersebut dapat dilihat pada gambar 1.1. Proses pengembangan dimulai dari sebuah spesifikasi (specification) dari sistem (software atau hardware) yang akan dibuat. Spesifikasi ini dibuat oleh pemberi pekerjaan, yang bisa sama dengan orang yang akan melakukan desain tetapi tidak harus sama. Spesifikasi ini kemudian akan diimplemen3 Terima kasih kepada Iwan Awaludin dari Polban yang menunjukkan kerancuan terminologi pada tulisan ini. Pada versi terdahulu, bagian ini disebut “proses desain”, padahal seharusnya adalah “proses pengembangan.” Hal ini sudah dikoreksi pada versi ini.
12
BAB 1. PENDAHULUAN
tasikan. Masalah yang timbul adalah bagaimana cara menuliskan spesifikasi agar dapat dimengerti oleh orang yang akan mengimplementasikan spesifikasi tersebut. Spesifikasi yang ditulis dalam bahasa natural (natural language), seperti bahasa Indonesia atau bahasa Inggris, sering membingungkan karena memiliki kerancuan makna (ambiguous). Untuk itu perlu dibuat sebuah standar formal untuk mendefinisikan spesifikasi software atau hardware. Pembahasan mengenai formal specification ini akan dibahas pada bab terpisah. Sebuah spesifikasi dapat diterjemahkan menjadi beberapa implementasi, n-implementations. Ada cara melakukan implementasi secara otomatis melalui automatic or automated synthesis atau implementasi secara manual4 . (Lihat gambar 1.1.) Sebuah implementasi dapat ditranslasikan menjadi implementasi lain melalui proses optimasi. Sebagai contoh, di dalam desain hardware kita dapat melakukan optimasi untuk menghemat area atau menghemat power. Hasil dari proses optimasi ini adalah implementasi lain yang sudah optimized. Pengertian translasi adalah perubahan pada satu level desain yang sama. Setelah implementasi selesai, maka tugas seorang desainer adalah menguji dan menjamin kebenaran dari implementasinya. Proses pengujian ini biasanya dilakukan dengan simulasi atau testing secara coba-coba atau adhoc. Testing dilakukan dengan mengambil sampel atau menguji dengan semua kombinasi (exhaustive test). Hal ini hanya dapat dilakukan untuk sistem yang berukuran kecil. Sebagai contoh, untuk sistem hardware digital yang memiliki empat (4) input, ada 24 atau 16 kombinasi yang harus dicoba. Angka ini cukup kecil untuk exhaustive test. Untuk sistem yang memiliki ukuran besar, misalnya mikroprosesor yang memiliki data 64-bit, exhaustive test tidak dapat dilakukan. Kombinasi 264 sudah sangat besar sekali. Dapat dibayangkan apabila kita harus menguji sistem yang memiliki 128-bit input. Apabila anda belum dapat membayangkan betapa besarnya angka tersebut, lihat tabel 1.3. Dapat dilihat bahwa kemungkinan anda mendapatkan lotre dan disambar petir lebih besar daripada menemukan bugs pada sebuah sistem yang memiliki jumlah bit 64-bit. Proses pengujian dengan menggunakan simulasi dan sampel dari data disebut sebagai validasi (validation). Sementara itu proses verifikasi (verification) adalah membuktikan secara matematis bahwa implementasi memang mengimplementasikan spesifikasi. Verifikasi secara formal menjamin bahwa implementasi memang mengimplementasikan spesifikasi. Namun masih ada kemungkinan bahwa spesifikasinya itu sendiri yang salah, yaitu bukan yang 4
Pada versi berikutnya akan diceritakan mengenai formal synthesis.
1.4. PRASYARAT PENGETAHUAN
13
Tabel 1.3: Bilangan besar [14] Besaran fisik Probabilitas terbunuh karena sambaran petir setiap harinya Probabilitas memenangkan hadiah pertama dari lotre di Amerika Serikat Probabilitas memenangkan hadiah pertama dari lotre di Amerika Serikat dan terbunuh oleh sambaran petir di hari itu juga Umur dari sebuah planet Umur dari universe Jumlah atom di planet
Besaran angka 1 in 9 billion (233 ) 1 in 228
1 in 261 230 234 2170
diinginkan oleh desainer. Karena spesifikasinya bukan yang diinginkan, maka implementasinya akan salah karena dia mengikuti spesifikasi tersebut, meskipun implementasi sudah diverifikasi. Jadi validasi masih dibutuhkan untuk memastikan bahwa implementasi memang yang diinginkan. Formal verification akan dibahas pada bab tersendiri.
1.4
Prasyarat Pengetahuan
Untuk mempelajari metoda formal secara baik dibutuhkan beberapa pengetahuan dasar seperti matematika, Finite Automata (FA) atau Finite State Machine (FSM), dan teori bahasa (seperti penggunaan notasi BNF, parser). Setiap pengetahuan tersebut di atas memiliki buku atau referensi yang lebih baik dari buku ini. Sayangnya buku-buku yang membahas hal tersebut biasanya ukurannya sangat tebal dan isinya agak “berat”. Contohnya: • Buku karangan K. Rosen untuk Discrete Math • Hopcroft dan Ullman Apabila memungkinkan, hal-hal yang dibutuhkan untuk memahami sebuah konsep yang ada di dalam buku ini akan dijelaskan dengan cara membuat sari atau rangkuman dari buku-buku tersebut di atas.
14
BAB 1. PENDAHULUAN
Bab 2
Formal Specification Seperti telah dijelaskan secara sepintas pada bab Pendahuluan, proses desain dimulai dari sebuah spesifikasi. Spesifikasi ini dibuat oleh pemberi pekerjaan yang kemudian akan diimplementasikan oleh seorang (atau satu tim) implementor. Spesifikasi dari sebuah sistem yang akan didesain dapat dituliskan dalam bahasa Inggris (atau natural language lainnya) dan kadang-kadang dilengkapi dengan diagram atau sketsa. Namun spesifikasi dalam bahasa natural ini memiliki kelemahan: • ambiguous atau memiliki banyak makna • sukar diproses secara otomatis (mechanized) Contoh suatu pernyataan atau spesifikasi yang ambiguous adalah sebagai berikut. Jika kita pergi ke sebuah restoran, ada sebuah pilihan: Sup atau sayur sudah termasuk dalam menu. Apakah yang dimaksud adalah salah satu saja (sup saja, atau sayur saja)? Ataukah keduanya? Kata “atau” di sini sangat rancu. Dia mungkin tidak tepat sama seperti OR dalam boolean logic dimana keduanya boleh ada, akan tetapi lebih tepat seperti exclusive OR atau XOR dimana hanya salah satu yang dipilih tapi tidak boleh dua-duanya. Spesifikasi yang dituliskan dalam bahasa natural tadi, karena kerancuannya, sulit untuk diproses secara otomatis oleh sebuah komputer misalnya. Jika kita dapat menggunakan notasi yang standar dalam penulisan spesifikasi, mungkin proses selanjutnya bisa diotomatisasi dengan lebih mudah. Sebagai contoh, Kimia mempunyai standar baku untuk menuliskan rumusrumus Kimia. 15
16
BAB 2. FORMAL SPECIFICATION
TODO: contoh-contoh notasi kimia Contoh lain yang dapat menunjukkan kemudahan notasi formal adalah penulisan rumus matematik. Sebagai contoh, Fermat’s Last Theorem dapat dijabarkan dalam kata-kata sebagai berikut: Tidak ada empat bilangan bulat yang memenuhi persamaan sebagai berikut. Bilangan pertama dipangkatkan bilangan keempat, ditambah bilangan kedua dipangkatkan bilangan keempat, sama dengan bilangan ketiga dipangkatkan bilangan keempat, dimana bilangan keempat lebih besar dari dua. Teorema di atas lebih mudah dituliskan sebagai berikut Tidak ada bilangan bulat x, y, z yang memenuhi persamaan xn + y n = z n , dimana n > 2. Untuk mengatasi masalah spesifikasi yang tidak jelas maka dibuatlah pendekatan yang disebut formal specification. Hal ini dilakukan dengan menggunakan notasi formal.
2.1
Notasi formal
Formal specification menggunakan notasi formal yang memiliki basis matematik serta memiliki syntax dan sematics yang jelas. Seringkali notasi formal ini memiliki format yang dapat diproses oleh komputer (machine readable format). Tujuannya adalah membuat proses verifikasi menjadi otomatis, yaitu melakukan perbandingan antara spesifikasi dengan implementasi secara otomatis oleh komputer. Pada bagian ini akan dibahas beberapa contoh notasi formal. Pemilihan notasi bergantung kepada beberapa hal: • expresiveness • kemudahan penggunaan (easy to use) Kemampuan ekspresi yang tinggi memudahkan untuk menulis spesifikasi sistem yang kompleks. Namun seringkali hal ini diimbangi dengan ketidakmudahan untuk menuliskan spesifikasi tersebut. Sebagai contoh, higherorder logic memiliki kemampuan ekspresi yang sangat fleksibel. Namun untuk menggunakan higher-order logic ini membutuhkan pengetahuan dan pengalaman yang tinggi (steep learning curve). Kesulitan ini memudahkan orang membuat kesalahan dalam menuliskan spesifikasi, atau spesifikasi itu susah dibaca dan dimengerti.
2.2. CSP
2.2
17
CSP
Communicating Sequential Processes (CSP) merupakan sebuah formalism yang dikembangkan oleh C.A.R. Hoare [5, 6]. CSP ini memiliki kemampuan ekspresi yang sangat baik. Namun sayangnya belum ada tools CSP yang mudah digunakan dan tersedia secara gratis. (Lihat bagian PROMELA.) Pada bahasa pemrograman tingkat tinggi, assignment merupakan sebuah hal yang sudah dimengerti dengan baik. Akan tetapi operasi input dan output belum dimengerti dengan baik. Assignment berhubungan dengan state di dalam (internal) sebuah sistem, sementara input dan output berhubungan dengan state di luar (external). CSP mencoba memberikan sebuah notasi untuk input dan output ini. Program konvensional ditargetkan untuk dijalankan pada satu prosesor. Saat ini mulai banyak sistem yang menggunakan prosesor lebih dari satu (multiprocessor), dimana prosesor ini saling berkomunikasi satu dengan lainnya. Komunikasi antar prosesor ini harus dapat dijabarkan dengan mudah dan tidak ambiguous. Itulah sebabnya perlu ada notasi input dan output. Communicating Sequential Processes (CSP) mencoba memecahkan masalah notasi untuk menjabarkan (menspesifikasi) sistem yang terdiri dari beberapa proses, dimana pada setiap proses ini ada program yang sifatnya berurut (sequential). Proses-proses ini saling berkomunikasisatu dengan lainnya melalui input dan output. Contoh penggunaan notasi ini akan dijelaskan lebih lanjut. CSP mengusulkan sebuah solusi, yaitu: • Dijkstra’s guarded command; • Perintah parallel, yang juga berdasarkan kepada Dijkstra’s parbegin; • Perintah input dan output dengan format yang sederhana; • dan gabungan hal di atas.
2.2.1
Konsep dan Notasi
Notasi dari CSP bisa dituliskan dengan menggunakan notasi BNF (BackusNaur form)1 . 1
Backus-Naur form, yang juga dikenal dengan istilah Backus normal form, merupakan sebuah metasyntax untuk menjelaskan context-free grammars. Istilah BNF diambil dari dua nama, yaitu John Backus dan Peter Naur. BNF banyak digunakan sebagai notasi untuk mendeskripsikan grammar dari bahasa pemrograman. BNF pertama kali digunakan untuk mendeskripsikan sintaks dari bahasa ALGOL 60. Sejarahnya, Backus pertama kali
