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 Container Station RIm menjadi lebih rumit, jika variabel tersebut langsung diimplementasi kan 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 dikembang kan 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.