Saya mencoba mengajari diri saya berbagai pendekatan untuk verifikasi perangkat lunak. Saya sudah membaca beberapa artikel. Sejauh yang saya pelajari, logika proposisional dengan temporal umumnya menggunakan pengecekan model dengan pemecah SAT (dalam sistem yang sedang berlangsung - reaktif), tetapi bagaimana dengan Logika orde pertama dengan temporal? Apakah ini menggunakan pembuktian teorema? Atau bisakah itu juga menggunakan SAT?
Setiap petunjuk untuk buku atau artikel untuk pemula dalam hal ini sangat dihargai.
Jawaban:
Logika urutan pertama tidak dapat diputuskan, sehingga penyelesaian SAT tidak benar-benar membantu. Yang mengatakan, ada teknik untuk memeriksa model terikat formula urutan pertama. Ini berarti bahwa hanya sejumlah objek tetap yang dapat dipertimbangkan ketika mencoba menentukan apakah rumusnya benar atau salah. Jelas, ini tidak lengkap, tetapi jika contoh tandingan ditemukan, maka itu benar-benar contoh tandingan.
Alat Paduan adalah salah satu alat yang memungkinkan model untuk dijelaskan dalam logika tingkat pertama (meskipun sintaks permukaan didasarkan pada model yang dijelaskan secara relasional) dan menggunakan pengecekan model terbatas untuk menemukan solusi. Pemecah SAT digunakan di bawah tenda. Satu ekstensi paduan memungkinkan model dengan karakter temporal, meskipun secara teknis tidak mendukung logika temporal.
Jika Anda ingin menjelajahi lebih lanjut, misalnya, untuk memverifikasi kebenaran program, maka Anda dapat melihat alat verifikasi program. Ini umumnya didasarkan pada logika Hoare (untuk alasan tentang kondisi pra dan pasca), mungkin diperpanjang dengan logika Pemisahan (untuk alasan tentang tumpukan). Logika ini umumnya tidak dapat dipastikan, sehingga diperlukan sejumlah interaksi antara manusia dan alat verifikasi. Beberapa contoh alat adalah:
sumber
Setelah membaca pertanyaan Anda satu-satunya cara saya bisa melihat dan memiliki pengetahuan yang cukup untuk mengikat topik bersama adalah untuk memberikan satu set artikel tingkat tinggi yang menelusuri dari verifikasi perangkat lunak yang berakhir dengan mencoba menyatukan pengecekan model dan pembuktian teorema. Semoga komentar saya melakukan itu:
Lihatlah verifikasi Perangkat Lunak kemudian Verifikasi formal lalu Pemeriksaan model dan Verifikasi Perangkat Lunak Formal: Pemeriksaan Model dan Pembuktian Teorema
Dave telah memberikan jawaban yang bagus sehingga saya tidak bisa melakukan lebih banyak keadilan untuk bagian pertama dari pertanyaan daripada yang dilakukan Dave, karena saya juga baru dalam hal ini.
Karena ini adalah pertanyaan pertama Anda di situs SE , alasan saya tidak memberikan jawaban tetapi komentar adalah karena di sini jawaban tidak hanya berupa sekumpulan tautan, tetapi harus memberikan jawaban tertulis dan menggunakan tautan untuk mendukung jawaban; dengan demikian komentar bukannya jawaban.
Berkaitan dengan:
Buku yang saya sarankan dan gunakan adalah:
Logika dalam Ilmu Komputer - Pemodelan dan Penalaran tentang Sistem 2nd Ed. oleh Huth dan Ryan Ini memperkenalkan logika dan bergerak ke atas untuk memeriksa model, tetapi tidak masuk ke pembuktian teorema. Jadi ini harus mencakup semua pertanyaan dasar Anda terkait dengan logika dan pengecekan model.
Prinsip-prinsip pengecekan model oleh Baier dan Katoen Saya baru saja mulai membaca yang ini, dan itu jauh lebih baik daripada membaca banyak makalah dan mencoba melihat bagaimana semuanya cocok. Ini adalah salah satu yang paling, jika bukan buku yang paling direkomendasikan tentang masalah pemeriksaan model. Ini harus menjawab pertanyaan Anda yang lebih lanjut tentang pengecekan model.
Logika temporal dan sistem negara oleh Kroger dan Merz Saya sering suka memiliki buku oleh penulis yang berbeda ketika belajar sendiri suatu subjek. Yang ini untuk melengkapi / melengkapi "Prinsip memeriksa model"
Buku pegangan logika praktis dan penalaran otomatis oleh Harrison Menjadi seorang programmer Saya tidak bisa merekomendasikan buku ini cukup. Buku ini dimulai dengan memperkenalkan logika dan bergerak sepanjang jalan melalui titik pembuatan kernel untuk sebuah teorema yang didasarkan pada karya HOL Light . Hanya untuk menggarisbawahi bahwa buku ini menggunakan kode OCaml yang berfungsi, jelaskan teorema dalam istilah yang saya temukan ramah dan memberi Anda apa yang perlu Anda ketahui tetapi tidak terlalu banyak sehingga Anda tidak dapat membuat koneksi atau merasa seperti Anda berlari di trek samping. If adalah buku yang sangat terfokus untuk beralih dari logika ke tipe teorema tertentu.
Cara membuktikannya: pendekatan terstruktur oleh Velleman Untuk masuk ke dalam pembuktian asisten untuk pembuktian teorema Anda perlu menghidupkan dan tidurkan teorema.
Pengantar Bukti dan Matematis Vokasional oleh Hari Ini adalah buku gratis yang tidak hanya melengkapi "Bagaimana membuktikannya", itu melampaui itu secara singkat. Saya tidak akan terkejut melihat yang satu ini menjadi populer.
Saat ini saya tidak dapat memperluas lebih lanjut tentang pembuktian teorema karena saya masih mempelajari pro / kontra dan masing-masing, tetapi yang saya fokuskan adalah
Isabelle karena didasarkan pada penyatuan tingkat tinggi.
Asisten pembuktian ini juga biasanya memiliki buku, terkini, populer, sumber terbuka, dipelihara, dan memiliki komunitas dukungan aktif.
Catatan: Saya menggunakan worldcat.org untuk referensi buku-buku, tetapi Anda dapat memeriksanya menggunakan fitur tampilan dalam Amazon.
sumber