Formal Modeling and Software Configuration Management

Cleanroom Software Engineering

• Increment Planning: menyusun rencana tambahan
• Requirment Gathering: mendefinisikan deskripsi dari level customer requirment
• Box Structure Spesification: menjelaskan spesifikasi fungsional
• Design Formal: Spesifikasi (BlackBox) yang iteratif halus untuk menjadi analog dengan desain arsitektur dan prosedural.
• Verifikasi Kebenaran Software
• Code Generation: spesifikasi struktur kotak, diwakili dalam bahasa khusus, ditransmisikan ke dalam bahasa pemrograman yang sesuai.
• Statistical Test Planning: statistik dari test case
• Statistical Usage Planning: mengeksekusi serangkaian tes yang berasal dari sampel statistik 
• Sertifikasi

Cleanroom Testing

• statistical use testing: menguji penggunaan aktual dari program
• menentukan “usage probability distribution”

• menganalisis spesifikasi untuk mengidentifikasi sebuah pergerakan
• pergerakan menyebabkan perangkat lunak untuk mengubah perilaku
• buat skenario pengunaan
• menetapkan probabilitas penggunaan untuk setiap pergerakan
• uji kasus dihasilkan untuk setiap pergerakan sesuai dengan distribusi penggunaan probabilitas 

Certification

1. Harus ada skenario pengunaan
2. Spesifikasikan profile pemakaian
3. Test case dihasilkan dari profile
4. Tes dieksekusi dan data kegagalan dicatat dan dianalisis
5. Reliability dihitung dan bersertifikat 

Certification Model

• Sampling model
• Component model
• Certification model

Formal Method

Formal Method yang digunakan dalam mengembangkan sistem komputer secara matematis untuk menggambarkan sifat sistem properties. Formal metode seperti menyediakan kerangka kerja di mana orang dapat menentukan, mengembangkan, dan memverifikasi sistem secara sistematis, bukan secara ad hoc.

Formal Spesification

• Desired Properties: konsistensi, kelengkapan, dan kurangnya ambiguitas adalah tujuan dari semua metode spesifikasi.
• Formal syntax: spesifikasi bahasa memungkinkan persyaratan atau desain untuk ditafsirkan hanya dengan satu cara, menghilangkan ambiguitas yang sering terjadi pada bahasa normal (misalnya, bahasa Inggris) atau notasi grafis harus ditafsirkan
• Fasilitas deskriptif set teori dan notasi logika memungkinkan pernyataan yang jelas dari fakta-fakta
• Konsistensi dipastikan dengan matematis membuktikan bahwa fakta-fakta awal dapat secara resmi dipetakan (menggunakan aturan inferensi) ke dalam laporan kemudian dalam spesifikasi.

Formal Methode Concept

• data invariant: suatu kondisi yang benar di seluruh pelaksanaan sistem yang berisi kumpulan data
• state
• operation: suatu tindakan yang terjadi dalam suatu sistem dan membaca atau menulis data ke state

Object Constraint Language (OCL)

• notasi formal dikembangkan sehingga pengguna dari UML dapat menambahkan lebih presisi dengan spesifikasi mereka
• Semua kekuatan logika dan diskrit matematika tersedia dalam bahasa tersebut
• Namun para perancang OCL memutuskan bahwa hanya karakter ASCII (bukan notasi matematika konvensional) harus digunakan dalam laporan OCL

OCL Overview

• Seperti bahasa pemrograman berorientasi objek, ekspresi OCL melibatkan operator yang beroperasi pada objek.
• Namun, hasil dari ekspresi lengkap harus selalu menjadi Boolean, yaitu benar atau salah.
• Object dapat contoh dari OCL Collection class, Set dan Squence adalah dua subclass.

Baseline merupakan tonggak dalam pengembangan perangkat lunak yang ditandai dengan pengiriman item konfigurasi satu atau lebih perangkat lunak dan persetujuan SCIs ini yang diperoleh melalui review teknis formal

Repository Features

• Versioning: memberikan versi pada program dan melakukan perubahan versi saat ada perubahan
• Dependency tracking and change management: repositori mengelola berbagai hubungan antara elemen data yang tersimpan di dalamnya.
• Requirment Tracing: menyediakan kemampuan untuk melacak semua desain dan konstruksi komponen dan kiriman yang dihasilkan dari spesifikasi kebutuhan spesifik
• Configuration Management: Melacak serangkaian konfigurasi yang mewakili tonggak proyek atau rilis produksi tertentu. manajemen versi menyediakan versi yang diperlukan, dan manajemen link melacak saling ketergantungan.
• Audit Trails: menetapkan informasi tambahan tentang kapan, mengapa, dan oleh siapa perubahan yang dibuat.

SCM Elements

• Component elements: seperangkat alat digabungkan dalam sistem manajemen file (misalnya, database) yang memungkinkan akses dan pengelolaan setiap item konfigurasi perangkat lunak.
• Process elements: koleksi prosedur dan tugas-tugas yang menentukan pendekatan yang efektif untuk mengubah manajemen (dan kegiatan terkait) untuk semua konstituen yang terlibat dalam manajemen, teknik dan penggunaan perangkat lunak komputer.
• Construction elements: suatu tools yang mengotomatiskan pembangunan software dengan memastikan bahwa set dari komponen divalidasi (yaitu, versi yang benar) telah dirakit.
• Human elements: untuk menerapkan SCM yang efektif, tim pembuaat software menggunakan suatu tools dan fitur proses (meliputi elemen CM lainnya).

Version Control ada 4hal yang harus diperhatikan dalam version control

• Project Database (repository) yang menyimpan semua konfigurasi objek yang relevan
• kemampuan manajemen versi yang menyimpan semua versi dari objek konfigurasi (atau memungkinkan versi yang akan dibangun menggunakan perbedaan dari versi terakhir);
• membuat fasilitas yang memungkinkan insinyur perangkat lunak untuk mengumpulkan semua konfigurasi object yang relevan dan membangun versi tertentu dari perangkat lunak.
• masalah pelacakan (juga disebut bug tracking) kemampuan yang memungkinkan tim untuk merekam dan melacak status dari semua isu yang beredar terkait dengan setiap konfigurasi object.