LogFire
Sistem berbasis aturan tampak alami untuk verifikasi runtime (RV)/pemantauan program. Dari sudut pandang notasi spesifikasi, sistem berbasis aturan tampaknya cukup cocok untuk mengekspresikan jenis properti yang biasanya ditulis oleh komunitas verifikasi runtime. Spesifikasi yang ditulis dalam sistem aturan memiliki cita rasa operasional, yang dapat dilihat sebagai kerugian atau keuntungan, tergantung pada sudut pandangnya. Rasa operasional membuat spesifikasi lebih panjang daripada logika temporal deklaratif atau ekspresi reguler; Namun, mereka alami untuk menulis. Setelah ide inti dikuasai, aturan penulisan menjadi mudah, seperti pemrograman. Spesifikasi yang lebih deklaratif bisa lebih sulit untuk diperbaiki. Pengamatan ini mirip dengan pengamatan bahwa mungkin lebih mudah untuk merumuskan properti nontrivial sebagai mesin keadaan daripada sebagai rumus logika temporal atau ekspresi reguler.
Penjelajah dan pesawat ruang angkasa JPL menghasilkan aliran telemetri saat beroperasi. Aliran telemetri pada dasarnya adalah urutan peristiwa yang disimpan di lapangan sebagai log dalam memori persisten. Operasi misi perlu menghasilkan pemeriksaan otomatis bahwa log ini benar. LogFire dapat digunakan untuk memeriksa log ini. LogFire, misalnya, memungkinkan insinyur operasi untuk secara otomatis memastikan bahwa penjelajah melakukan langkah-langkah yang benar.
LogFire membaca dalam file log dan memeriksanya dengan spesifikasi formal. Spesifikasi dapat dirumuskan dalam bahasa berbasis aturan. Bahasa spesifikasi berbasis aturan diimplementasikan sebagai API dalam bahasa pemrograman Scala. Ini menghasilkan bahasa spesifikasi yang sangat kuat karena seseorang dapat mencampur aturan dan pemrograman tradisional.
Definisi bahasa berbasis aturan sebagai API di Scala memiliki tampilan DSL (Bahasa Khusus Domain) karena dukungan Scala untuk definisi DSL (internal) tersebut. Mesin aturan, yang didasarkan pada algoritme RETE yang terkenal, selain itu telah ditambah dengan gagasan tentang peristiwa, yang seketika berbeda dengan fakta berumur panjang yang biasanya digunakan oleh mesin aturan. Terakhir, metode pengindeksan telah mengoptimalkan mesin untuk menangani peristiwa yang membawa data.
LogFire selanjutnya memungkinkan pola spesifikasi untuk dengan mudah dikodekan untuk menghasilkan aturan. Relatif mudah untuk mendefinisikan pola spesifikasi sebagai fragmen logika temporal dan garis waktu — contoh yang diterjemahkan ke aturan. Nuansa yang menarik adalah bahwa template ini memungkinkan peristiwa berparameter data. Eksperimen telah dilakukan dengan membandingkan implementasi yang dihasilkan dengan enam sistem berbasis aturan dan verifikasi runtime lainnya.
NASA berusaha untuk melisensikan perangkat lunak ini secara bebas dan membuatnya tersedia untuk penggunaan umum untuk proyek sumber terbuka. Silakan hubungi NASA's Licensing Concierge di Alamat email ini dilindungi dari robot spam. Anda perlu mengaktifkan JavaScript untuk melihatnya., atau hubungi kami di 202-358-7432 untuk memulai diskusi lisensi.
