Anda Tidak Membutuhkan LTL untuk Menggunakan Model Checker

Anda tidak perlu mempelajari logika temporal linear untuk menggunakan model checker. Alat seperti Kani, CBMC, dan Alloy memungkinkan Anda memverifikasi properti dengan assertion dan constraint relasional biasa. Anda mengorbankan kemampuan untuk membuktikan properti liveness demi kurva pembelajaran yang diukur dalam jam, bukan minggu, dan untuk sebagian besar bug perangkat lunak, itu adalah pertukaran yang layak dilakukan.

Temporal Logic Adalah Penjaga yang Diminta oleh Sebagian Besar Model Checker

Model checker klasik, SPIN dan NuSMV, meminta Anda mengekspresikan properti dalam LTL atau CTL. Anda menulis sesuatu seperti G(request -> F(response)) yang berarti “secara global, setiap permintaan pada akhirnya diikuti oleh respons.” Ini sangat powerful. Ini dapat membuktikan bahwa protocol Anda tidak pernah mengalami deadlock, bahwa setiap pesan pada akhirnya diakui, bahwa sistem Anda fair.

Ini juga keterampilan khusus yang tidak dimiliki oleh sebagian besar pengembang yang sedang bekerja. Membaca formula LTL tidak seperti membaca kode. Operator-nya bersifat modal, semantiknya berada pada trace tak terbatas, dan intuisi yang Anda bangun saat menulis unit test tidak dapat ditransfer. Jadi pertanyaannya adalah adil: jika Anda menginginkan kekuatan bug-finding dari model checking, apakah Anda benar-benar harus memanjat gunung itu terlebih dahulu?

Tidak. Kelas alat yang berbeda telah ada selama beberapa dekade, dan mereka memverifikasi kode dengan assertion yang sama yang sudah Anda tulis.

Bounded Model Checker Mengubah Assertion Menjadi Masalah SAT

Bounded model checker tidak meminta Anda mempelajari logika baru. Mereka meminta Anda menulis test harness. Anda mendeklarasikan input nondeterministik, membatasinya dengan assumption, dan menegaskan properti dalam bahasa host. Alat tersebut kemudian membuka loop hingga batas tertentu, mengenkode program sebagai formula SAT atau SMT, dan meminta solver menemukan counterexample.

Jika solver mengembalikan UNSAT, properti Anda berlaku untuk semua path dalam batas tersebut. Jika menemukan counterexample, Anda mendapatkan trace konkret yang menunjukkan persis input mana yang memicu bug. Tidak ada operator temporal. Tidak ada trace tak terbatas. Hanya assertion yang gagal dengan vector input yang dapat direproduksi.

Kani adalah bounded model checker yang paling mudah diakses untuk Rust. Ini diinstal dengan cargo install kani-verifier dan berfungsi pada kode Rust biasa.

Contoh Nyata: Memeriksa State Machine di Rust

Berikut adalah state machine dengan bug. Ini melacak counter sederhana yang berkurang pada setiap tick hingga mencapai nol, kemudian bertransisi kembali ke idle.

#[derive(Clone, Copy, PartialEq, Debug)]
enum State {
    Idle,
    Running,
    Stopped,
}

struct Machine {
    state: State,
    count: u32,
}

impl Machine {
    fn start(&mut self, initial: u32) {
        if self.state == State::Idle && initial > 0 {
            self.state = State::Running;
            self.count = initial;
        }
    }

    fn tick(&mut self) {
        if self.state == State::Running {
            self.count -= 1;
            if self.count == 0 {
                self.state = State::Idle;
            }
        }
    }

    fn stop(&mut self) {
        if self.state == State::Running {
            self.state = State::Stopped;
        }
    }
}

Bug-nya halus. Lihat stop. Ini mengatur state menjadi Stopped tetapi membiarkan count tidak berubah. Jika sesuatu kemudian mengasumsikan count == 0 ketika state == State::Stopped, asumsi tersebut salah.

Berikut adalah Kani proof harness yang menangkapnya:

#[kani::proof]
fn check_stopped_implies_count_zero() {
    let mut machine = Machine {
        state: State::Idle,
        count: 0,
    };

    let initial: u32 = kani::any();
    kani::assume(initial > 0 && initial <= 10);

    machine.start(initial);
    machine.tick();
    machine.stop();

    assert!(
        machine.state != State::Stopped || machine.count == 0,
        "Stopped state should have count == 0"
    );
}

Kani menjelajahi setiap path. Ia menemukan bahwa jika initial == 2, setelah start mesin berada dalam Running dengan count == 2. Satu tick mengurangi count menjadi 1 tetapi state tetap Running. Kemudian stop mengatur state menjadi Stopped dengan count == 1. Assertion gagal. Kani melaporkan trace persis ini.

Ini adalah pengalaman model checking tanpa temporal logic. Anda menulis Rust. Anda menulis assertion dalam Rust. Alat tersebut memberi tahu Anda input mana yang membatalkannya.

Alloy Menemukan Bug pada Level Desain dengan Logika Relasional

Bounded model checker memverifikasi kode. Alloy memverifikasi desain.

Alloy adalah model finder, bukan model checker tradisional, tetapi perbedaannya kurang penting dibandingkan workflow-nya. Anda menggambarkan sistem Anda sebagai sekumpulan relasi, invariant state sebagai constraint logika first-order, dan meminta Alloy menemukan counterexample. Ia mencari semua instance yang mungkin hingga scope yang ditentukan pengguna dan menunjukkan diagram kegagalan kepada Anda.

Berikut adalah model Alloy dari properti graf berarah sederhana:

sig Node {
    next: set Node
}

pred reachable[n1, n2: Node] {
    n2 in n1.^next
}

assert symmetric_reachability {
    all n1, n2: Node |
        reachable[n1, n2] implies reachable[n2, n1]
}

check symmetric_reachability for 3

Assertion tersebut menyatakan bahwa reachability bersifat simetris. Alloy memeriksa ini untuk semua graf dengan hingga tiga node dan segera menggambar counterexample: graf di mana n1 menunjuk ke n2 tetapi n2 tidak memiliki edge keluar. Operator G, F, atau U tidak muncul di mana pun.

Apa yang Anda Korbankan: Liveness dan Perilaku Tak Terbatas

Kemudahan ini memiliki biaya. Bounded model checker hanya memverifikasi perilaku hingga loop bound atau panjang trace tertentu. Mereka tidak dapat membuktikan bahwa permintaan pada akhirnya dijawab, hanya bahwa hal buruk tidak terjadi dalam N langkah pertama. Alloy hanya memeriksa instance dalam scope-nya. Ia tidak dapat membuktikan properti untuk sistem yang secara sewenang-wenang besar, hanya bahwa tidak ada counterexample di bawah batas tersebut.

Jika Anda perlu membuktikan bahwa protocol consensus Anda tidak pernah kehilangan write yang telah di-commit, atau bahwa setiap pesan pada akhirnya dikirim, Anda masih membutuhkan temporal logic dan unbounded model checking. Alat seperti TLA+ membungkus temporal logic dalam sintaks yang terlihat lebih seperti matematika daripada logika modal, tetapi semantik yang mendasarinya tetap temporal.

Untuk invariant struktur data, enforcement kontrak API, dan menemukan race condition yang hanya dipicu pada path eksekusi ke-47, alat bounded biasanya cukup. Mereka menangkap bug yang terlewat oleh unit test, dan mereka melakukannya dengan assertion yang dapat Anda baca tanpa buku teks.

Memulai dengan Kani dalam Lima Menit

Jika Anda telah menginstal Rust, bounded model checking hanya berjarak satu perintah.

cargo install kani-verifier
cargo kani setup

Buat crate baru, tulis fungsi dengan bug halus, dan tambahkan harness #[kani::proof]. Jalankan cargo kani. Jika Kani menemukan counterexample, ia mencetak input konkret yang memicu kegagalan. Jika ia melaporkan VERIFICATION SUCCESSFUL, properti Anda berlaku untuk semua path dalam batas default.

Mulailah dengan fungsi yang memiliki state space kecil dan invariant yang jelas. State machine, validasi parser, dan transisi state protocol adalah target pertama yang ideal. Hindari mencoba memverifikasi seluruh server HTTP pada upaya pertama Anda. SAT solver memiliki batas, dan kesabaran Anda juga.

FAQ: Bounded vs. Unbounded, Liveness, dan Memulai

Apakah bounded model checking sebenarnya model checking?

Secara teknis, ini adalah varian yang mengenkode masalah sebagai satisfiability query daripada menjelajahi state graph secara eksplisit. Bagi pengembang yang mencoba menemukan bug, perbedaannya bersifat akademis. Ini menjelajahi semua path secara sistematis, yang secara praktis merupakan arti dari model checking.

Bisakah saya membuktikan liveness dengan Kani atau CBMC?

Tidak langsung. Properti liveness memerlukan penalaran tentang perilaku tak terbatas, dan alat bounded secara eksplisit membatasi pencarian mereka. Anda kadang dapat mengenkode pemeriksaan liveness bounded dengan membuka cukup banyak langkah untuk mencapai fixpoint, tetapi itu adalah teknik lanjutan.

Bagaimana dengan TLA+? Apakah itu memerlukan temporal logic?

TLA+ menggunakan Temporal Logic of Actions, jadi ya, secara teknis. Tetapi Leslie Lamport merancang sintaksnya agar terbaca seperti matematika biasa. Sebagian besar spesifikasi TLA+ menghabiskan 90% teksnya pada invariant state dan constraint struktur data, bukan pada operator temporal. Ini adalah jalur paling mudah diakses jika Anda memerlukan temporal reasoning yang unbounded.

Haruskah saya menggunakan Alloy atau Kani?

Gunakan Kani jika Anda memiliki kode Rust dan ingin memverifikasi detail implementasi. Gunakan Alloy jika Anda masih dalam tahap mendesain sistem dan ingin mengeksplorasi apakah invariant Anda bahkan mungkin sebelum menulis kode.

Pilih Alat yang Cocok dengan Masalah Anda, Bukan Ambisi Anda

Temporal logic indah dan powerful, tetapi ini bukan prasyarat untuk verifikasi formal. Bounded model checker dan relational model finder memungkinkan Anda mengekspresikan properti dalam bahasa yang sudah Anda kenal. Mereka tidak akan membuktikan bahwa sistem Anda pada akhirnya berhenti, tetapi mereka akan menemukan kesalahan off-by-one yang merusak state machine database Anda. Untuk sebagian besar tim, itulah bug yang penting.

Mulailah dengan Kani pada satu fungsi berstate. Tulis satu assertion. Biarkan solver memberi tahu Anda apa yang Anda lewatkan.