EC 7030 - Metoda Formal

Menu

Dosen: Budi Rahardjo
Waktu: Senin, 13:00-15:00
Tempat: lab sistem, PAUME, lantai 4 gedung PAU

Silabus

Update: 28 Maret 2005

:: info ::

Kuliah ini merupakan perubahaan dari kuliah EL688 yang diselenggarakan tahun lalu. Untuk sementara ini lihat halaman kuliah EL688 untuk mendapatkan materi kuliah dan bahan bacaan. Secara berangsur-angsur, informasi akan saya pindahkan ke halaman ini.

:: berita ::

Tanggal 28 Maret 2005, tidak ada kuliah.
Mohon maaf atas keterlambatan informasi ini. Anda ditugaskan untuk membaca materi PROMELA dan SPIN, khususnya untuk praktikum. Anda pun bisa memulai praktikum sendiri jika anda telah berhasil memasang SPIN di komputer anda.

Tanggal 7 Maret 2005, hari Senin, tidak ada kuliah.

Di bawah garis ini merupakan informasi untuk kelas tahun lalu. Tidak usah diperhatikan.

Daftar proyek akhir sudah tersedia di sini. Perhatikan apakah nama anda sudah terdaftar dalam daftar tersebut. Jika belum, hubungi saya dan/atau kirimkan proposal / laporan anda kembali.

Hasil dari lab KBDD anda dapat dilihat di sini. Silahkan gunakan (download) untuk keperluan laporan anda.

Beberapa orang sudah mengirimkan alamat email anda untuk dimasukkan ke dalam milis. Yang belum, harap mengirimkan alamat email anda ke saya. Yang sudah mengirimkan email M. Amien, tatyantoro andrasto, Velix Sutanto, Andriana, Taufik Siswanto, Denny Tresna Seswara. Ada seorang lagi yang hilang emailnya. Kita diskusikan ini di kelas.

Yang baru

:: Materi ::

Formal Specification

  1. Communicating Sequential Processes (CSP)
    Referensi: C.A.R. Hoare, "Communicating Sequential Processes," Communications of the ACM, Vol. 21, No. 8, pp. 666-677, August 1978. (ukuran file agak besar, 1,2MBytes)
  2. PROMELA dan SPIN
    Informasi mengenai PROMELA dan SPIN ada di Bell-Labs.
    Paper Holzmann tentang PROMELA dan SPIN dalam bentuk PDF saya secara lokal di sini.
    Pengantar (introduction) PROMELA dan SPIN (baru)
    Laboratorium dengan menggunakan program SPIN.
    Manual laboratorium (dalam format Star/OpenOffice) (dalam format PDF)
  3. Binary Decision Diagram (BDD)
    Bahan bacaan utama dari paper R. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Transaction on Computers, Vol.C-35, No. 8, August 1986. (Copy di sini untuk memudahkan download dalam format PDF)
    Technical Report dari CMU
    Bahan bacaan lain: Formal Hardware Verification with BDD (A. Hu).
    Laboratorium dengan menggunakan KBDD. Source code (bdd.4.2.tar.Z) ada di sini (untuk sistem UNIX). Manual lab dalam format RTF.
  4. Specification and Description Language (SDL)
    Materi presentasi (power point).
    Referensi lain dapat diperoleh dari situs web SDL Forum. Berikut ini adalah link ke tutorial SDL dari Dr. Holz. (Koleksi lokal ada di sini.)
  5. Higher Order Logic (HOL)
    Materi presentasi (power point)
  6. Petri Nets (jika waktunya cukup)