\chapter{Pendahuluan} Buku ini merupakan panduan kuliah Metoda Formal (dalam desain perangkat keras) atau {\em Formal Methods for Hardware Design} yang diberikan oleh Departemen (Jurusan) Teknik Elektro ITB. Buku ini merupakan kelanjutan dari {\em technical report}~\cite{budi99} yang merupakan hasil dari Riset Unggulan Terpadu (RUT) dan rangkuman dari beberapa makalah yang relevan dengan bidang metoda formal ini. \footnote{Buku ini masih dalam proses penulisan sehingga masih banyak bagian yang belum selesai. Proses penulisan menggunakan \LaTeX yang belum terkonfigurasi untuk bahasa Indonesia. Untuk itu anda akan menemukan beberapa kejanggalan pada pemenggalan kata.} Beberapa bagian dari buku ini membutuhkan latar belakang matematika diskrit dan {\em logic}. Agar bisa berdiri sendiri, buku ini memberikan beberapa pengantar tentang matematika diskrit dan {\em 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~\cite{rosen}. 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. \section{Latar Belakang} \begin{quote} {\em ``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) \end{quote} 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)\footnote{Banyak istilah asing yang dipaksakan diterjemahkan ke dalam bahasa Indonesia. Hasilnya justru malah membingungkan. Istilah {\em software} akan digunakan dalam buku ini agar tidak membingungkan.}. 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 {\em trend}nya menunjukkan tanda-tanda makin meningkat. Sebagai contoh, software {\em wordprocessor Wordstar} (WS) dahulu cukup dimasukkan ke dalam disket dalam ukuran 300~KBytes. Sementara ini, program {\em Microsoft Word 2000} harus didistribusikan dalam CD-ROM yang ukurannya ratusan MBytes. Sebagai gambaran, tabel~\ref{tabel:software} menunjukkan perkembangan kompleksitas dari operating system Microsoft Windows. Kompleksitas dalam tabel tersebut ditunjukkan dengan banyaknya jumlah baris kode ({\em lines of code (LOC)}). Sebagai perkiraan, setiap KLOC dapat memiliki 5 sampai dengan 50 bugs. \begin{table} \center \caption{Perkembangan kompleksitas software} \label{tabel:software} \begin{tabular}{|l|c|l|} \hline Sistem Operasi & Tahun & Jumlah Baris\\ & & (lines of code)\\ \hline 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\\ \hline \end{tabular} \end{table} \begin{table} \center \caption{Kompleksitas software lainnya~\cite{hoglund}} \label{table:software2} \begin{tabular}{ll} Sistem & Jumlah Baris Kode\\ \hline 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\\ \hline \end{tabular} \end{table} Jumlah transistor dalam sebuah {\em Integrated Circuit} (IC) sudah mencapai jutaan transistor. Pentium chip memiliki jutaan transistor. Kesemuannya 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 ({\em bugs}) dan mempercepat waktu yang dibutuhkan untuk mengembangkan dan memasarkan. {\em Time to market} di dunia yang {\em high-tech} ini sangat sempit. Khususnya untuk aplikasi yang membutuhkan keandalan tinggi (yang sering disebut {\em 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 ({\em 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 {\em rigorous}. \section{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 ({\em bugs}) pada software dan/atau hardware. Akibat yang ditimbulkan oleh kesalahan ini bervariasi dari ketidak-nyamanan ({\em inconvenience}) sampai korban jiwa (fatal). \begin{enumerate} \item {\bf 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~\cite{wiener}. \item {\bf 10 April 1981.} {\em 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:~\cite{peterson95}. \item {\bf 25 Februari 1991.} Di bidang militer, Patriot Amerika gagal menanggulangi roket {\em 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. {\em Patriot missile defense system} menggunakan software untuk melakukan {\em 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. Persamaan yang digunakan untuk melakukan {\em 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 berturut-turut sehingga timingnya sudah bergeser sebesar 36/100 detik (sudah cukup besar). Kesalahan ini sebetulnya sudah diketahui, akan tetapi perbaikan ({\em upgrade}) yang dikerjakan di {\em 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~\cite{wiener}. \item {\bf 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 {\em 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 {\em crash}. Sumber~\cite{wiener}. \item {\bf 4 Juni 1996.} Roket Ariane 5 meledak 40 detik setelah diluncurkan. Sumber informasi: European Space Agency (www.esa.int). \item 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 {\em design errors}. Sumber informasi: ACM Software Engineering Notes 8 (3). \item {\bf 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.\\ Sumber berita: http://news.bbc.co.uk/1/hi/uk/3772663.stm\\ http://www.nats.co.uk/news/news\_stories/2004\_06\_03.html \item {\em 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. \item {\em 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. \item {\em 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. \item {\bf 1988.} {\bf 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 ({\em tracking software}) yang memperagakan output yang tidak dapat dimengerti ({\em cryptic}) sehingga mengambil kesimpulan yang salah. \end{enumerate} Selain kasus-kasus di atas, sebetulnya masih banyak kecelakaan lain yang terjadi di dunia {\em engineering} yang tidak terkait dengan hardware atau software. Buku Henry Petroski~\cite{petroski92} 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 {\em comp.risk} juga banyak menceritakan kecelakaan yang diakibatkan oleh salah desain. \section{Proses Desain} Secara umum, proses desain meliputi beberapa tahap; spesifikasi ({\em specification}), implementasi ({\em implementation}), dan validasi ({\em validation}) serta verifikasi ({\em verification}). Kegiatan lain yang terkait dengan tahapan tersebut antara lain adalah {\em automated systhesis} dan {\em translation}. Kerangka tahapan tersebut dapat dilihat pada gambar~\ref{figure:proses}. \begin{figure} \epsfig{file=proses.eps} \caption{Diagram proses desain} \label{figure:proses} \end{figure} Proses desain dimulai dari sebuah spesifikasi ({\em 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 diimplementasikan. Masalah yang timbul adalah bagaimana cara menuliskan spesifikasi agar dapat dimengerti oleh orang yang akan mengimplementasikan spesifikasi tersebut. Spesifikasi yang ditulis dalam bahasa natural ({\em natural language}), seperti bahasa Indonesia atau bahasa Inggris, sering membingungkan karena memiliki kerancuan makna ({\em ambiguous}). Untuk itu perlu dibuat sebuah standar formal untuk mendefinisikan spesifikasi software atau hardware. Pembahasan mengenai {\em formal specification} ini akan dibahas pada bab terpisah. Sebuah spesifikasi dapat diterjemahkan menjadi beberapa implementasi, {\em n-implementations}. Ada cara melakukan implementasi secara otomatis melalui {\em automatic or automated synthesis} atau implementasi secara manual\footnote{Pada versi berikutnya akan diceritakan mengenai formal synthesis.}. (Lihat gambar~\ref{figure:proses}.) Sebuah implementasi dapat {\em 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 {\em 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 {\em ad-hoc}. Testing dilakukan dengan mengambil sampel atau menguji dengan semua kombinasi ({\em exhaustive test}). Hal ini hanya dapat dilakukan untuk sistem yang berukuran kecil. Sebagai contoh, untuk sistem hardware digital yang memiliki empat (4) input, ada $2^4$ atau 16 kombinasi yang harus dicoba. Angka ini cukup kecil untuk {\em exhaustive test}. Untuk sistem yang memiliki ukuran besar, misalnya mikroprosesor yang memiliki data 64-bit, {\em exhaustive test} tidak dapat dilakukan. Kombinasi $2^{64}$ 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~\ref{table:largenumber}. Dapat dilihat bahwa kemungkinan anda mendapatkan lotre dan disambar petir lebih besar daripada menemukan bugs pada sebuah sistem yang memiliki jumlah bit 64-bit. \begin{table} \caption{Large numbers~\cite{schneier96}} \label{table:largenumber} \center \begin{tabular}{|l|l|} \hline {\bf Besaran fisik} & {\bf Besaran angka}\\ \hline \hline Probabilitas terbunuh karena sambaran petir & \\ setiap harinya & 1 in 9 billion ($2^{33}$)\\ \hline Probabilitas memenangkan hadiah pertama dari & \\ lotre di Amerika Serikat & 1 in $2^{28}$\\ \hline Probabilitas memenangkan hadiah pertama dari & \\ lotre di Amerika Serikat dan terbunuh & \\ oleh sambaran petir di hari itu juga & 1 in $2^{61}$\\ \hline Umur dari sebuah planet & $2^{30}$\\ Umur dari universe & $2^{34}$\\ Jumlah atom di planet & $2^{170}$\\ \hline \end{tabular} \end{table} Proses pengujian dengan menggunakan simulasi dan sampel dari data disebut sebagai validasi ({\em validation}). Sementara itu proses verifikasi ({\em 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 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.