Sonlu durum sistemleri için sembolik bir model doğrulayıcısının gerçekleştirimi

Abstract

IV ÖZET Bu tezde sonlu durum sistemleri için sembolik bir model doğrulayıcı DOS ortamında C dilinde gerçekleştirilmiştir. Bir sistemin belirli bir özelliği sağlayıp sağlamadığının denetimi olarak tanımlanan doğrulama problemi ve özel olarak model doğrulama yöntemi incelenmiştir. Genel bir yaklaşım çerçevesinde ifade gücü yüksek mü-hesabı için bir model doğrulama yöntemi tanımlanmıştır. Sonlu durum sistemlerinin doğrulamasında ortaya çıkan durum patlaması probleminin çözümü için ikil karar şemaları kullanılmıştır. Boole cebri için tanımlanan ikil karar şemaları Boole fonksiyonlarının gösteriminde ekonomik yapılar üretilmesini olanaklı kılarlar. İkil karar şemalarının kullanımı ile sistem bilgileri olası en küçük boyutlarda saklanır. Böylelikle daha fazla durumlu sistemlerin doğrulamasının yapılması mümkündür. Yöntem bu alanda en yaygın olarak kullanılan yapı olan Zamansal Mantık ile karşılaştırılmış ve Zamansal Mantık formüllerinin mü-hesabmda gösterimleri tanımlanmıştır. Gerçekleştirimde kullanım kolaylığını sağlayacak ve zaman ve yer karmaşıklığını azaltacak gelişmeler belirtilmiştir. ANAHTAR KELİMELER Doğrulama, Model Doğrulama, İkil Karar Şemaları, Mü-hesabı, Zamansal Mantık

ABSTRACT In this thesis a symbolic model checker for finite state systems is implemented using C on DOS environment. Verification problem which is the process of checking whether a system meets a specified property and specifically the model checking method are investigated. A model checking method is defined in a general framework for mu-calculus which has high expressivity. For the solution of the state explosion problem which occurs in the verification of finite state systems binary decision diagrams are used. Binary decision diagrams that are defined for Boolean algebra allow to produce economical structures in the representation of Boolean functions. By the usage of binary decision diagrams system data are stored in smallest possible sizes. So that it is possible to verify the systems with more states. Method is compared with the Temporal Logic which is the most popular structure in this area and the representation of Temporal Logic formulas in mu-calculus are defined. Improvements which allows usage simplicity and reduction in the time and space complexity are stated. KEYWORDS Verification, Model Checking, Binary Decision Diagrams, Mu-calculus, Temporal Logic