Pemodelan logika pemeriksaan temporal linier dengan Buchi Automata

SIHITE, Liston, Drs. Retantyo Wardoyo, MSc.,Ph.D

2004 | Tesis | S2 Ilmu Komputer

Kebenaran dan kehandalan adalah dua kata kunci keberhasilan sebuah perancangan sistem perangkat keras maupun perangkat lunak. Untuk mendapatkan sistem yang benar dan handal, maka sistem harus melalui pengujian yang ketat terhadap seluruh komponennya Salah satu metode pengujian sistem yang baik adalah melalui pemodelan tingkah laku sistem, yang disebut model pemeriksaan (Model Checking), karena metode ini memungkinkan untuk melakukan pemeriksaan bagian demi bagian dalam sistem, sehingga dapat menjamin kehandalan sistem secara keseluruhan. Mekanisme model pemeriksaan ini adalah dengan memformulasi sifat-sifat sistem secara logika ke dalam bentuk logika proposisional. Automata adalah sebuah model aljabar yang terdiri dari state-state dan tansisi antar state. Satu model automata yang mengakomodir sebuah transisi yang tidak berhingga atau transisi yang melalui state final tidak berhingga kali, disebut Buchi Automata. Sistem-sistem reaktif bersifat terus-menerus bereaksi terhadap lingkungannya dengan proses yang tidak pernah berhenti (non terminating). Pemeriksaan dilakukan terhadap kejadian antar waktu dalam sistem, dengan demikian proses dalam sistem ini bersifat temporal, dan model yang memenuhi keadaan ini disebut Model Logika Temporal. Jika pemeriksaan dilakukan dari waktu ke waktu, modelnya disebut Model Logika Temporal Linier (MLTL) yang terdiri dari tupel M = (S, R, Label ) . MLTL ini kemudian diformulasi kedalam bentuk logika proposisional sehingga terbentuk model yang disebut Logika Proposisional Temporal Linier (LPTL). LPTL dalam bentuk logika dikonstruksi melalui sebuah eksplorasi graph dan Buchi automata, sehingga LPTL dapat dinyatakan dalam sebuah model Automata yang terdiri dari tupel Aw =(rumus) . Mekanisme ini disebut Pemodelan Logika Pemeriksaan Temporal Linier dengan Buchi Automata..

Correctness and reliability is two keywords successibilites of design both hardware and software systems. To get correct and reliability systems, it must be tight checking and testing overall components. Once of better checking method is modeling system behavioral, called Model Checking, this method possibly check system components part by part, so reliability of its overall components could be guarantee. The model checking mechanism is formulating system behavioral in logic sound and prepositional logic. Automata is an algebra model contents states, also transition between states. An automata model that accepting infinite states sequins transition or transition through final state infinitely often, is Buchi Automaton. Reactive systems characterized with its continuous reaction with environment and non-terminating. If checking does for behavioral system time to time, then the process in system considering like temporal habit, model which is satisfying this behavioral called Model Temporal Logic. If checking does for time to time as linear, then model called Model Linear Temporal Logic (MLTL) on topple . MLTL constructed using graph exploration and Buchi automaton then MLTL can be stated in an automata on topple A M = (S, R, Label ) (formula). This mechanism called Logic Checking Linear Temporal Modeling with Buchi Automata.

Kata Kunci : Komputer, Metode Pengujian Sistem, Buchi Automata, Modeling, Checking, Reactive system, Temporal Logic, Automaton.