| Metode B adalah metode formal yang digunakan dalam pengembangan piranti lunak mulai dari membuat spesifikasi, merancang, dan membuat kode program. Pengembangan piranti lunak dengan metode B dilakukan dengan cara mengubah spesifikasi formal yang masih abstrak menjadi lebih kongkrit. Proses ini dilakukan dengan menambahkan detil sedikit demi sedikit kedalam spesifikasi sehingga pada akhirnya menjadi spesifikasi yang dapat diterjemahkan langsung menjadi program komputer. Proses yang mengubah spesifikasi menjadi lebih kongkrit ini disebut dengan refinement. Pelaksanaan Tugas Akhir ini bertujuan untuk menelaah pengembangan spesifikasi, refinement, dan verifikasi dengan menggunakan metode B. Spesifikasi formal yang dikembangkan
adalah spesifikasi suatu sistem informasi bongkar-muat barang. Spesifikasi tersebut dikembangkan sesuai dengan deskripsi Container Station yang diajukan oleh Elena Troubytsna. Alat bantu pengembangan yang digunakan adalah Atelier B. Pengembangan Container Station diawali dengan menerjemahkan deskripsi ke dalam mesin abstrak ContainerStation. Mesin tersebut mengalami refinement hingga mesin implementasi dengan urutan: (1) ContainerStation, (2) ContainerStationR, (3) ContainerStationRIm. Beberapa variabel abstrak dalam ContainerStationR akan membuat detil implementasi dan bentuk proof obligation dalam ContainerStationRIm menjadi lebih rumit, jika variabel tersebut langsung diimplementasikan dengan struktur data yang disediakan Atelier B. Hal ini diatasi dengan membangun mesin lain, CART FUNCTION dan CART SET, untuk merepresentasikan struktur data yang sesuai dengan variabel-variabel tersebut. Verifikasi terhadap mesin-mesin yang dikembangkan dilakukan dengan membuktikan proof obligations dari mesin-mesin tersebut. Pembuktian proof obligations dilakukan secara
otomatis dan interaktif dengan menggunakan Atelier B. Dalam pembuktian interaktif, dikembangkan beberapa user theory untuk menyederhanakan proses pembuktian. Mesin CART FUNCTION dan CART SET berhasil dibuktikan dan dibangkitkan kode programnya
dalam bahasa C. Pengembangan ContainerStationRIm terhambat pada pembuktian beberapa proof obligations yang cukup kompleks. |