Specification and formal verification of fuzzy information processing for the case of edge detection
Kenar algılama durumu icin bulanık bilgi işlemenin belirlenmesi ve resmi olarak doğrulanması
- Tez No: 956680
- Danışmanlar: PROF. DR. MİECZYSLAW MİTCH KOKAR
- Tez Türü: Yüksek Lisans
- Konular: Elektrik ve Elektronik Mühendisliği, Electrical and Electronics Engineering
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2009
- Dil: İngilizce
- Üniversite: Northeastern University
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Elektrik ve Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Elektrik ve Bilgisayar Mühendisliği Bilim Dalı
- Sayfa Sayısı: 134
Özet
Bu tez, bir bilgi füzyon sisteminin inşa edilmeden önce nasıl doğrulanabileceğini araştırmaktadır. Bu amaca yönelik olarak, bir sistem önce biçimsel bir dilde matematiksel olarak tanımlanır. Tanım daha sonra çeşitli varsayımlar (teoremler) formüle edilerek ve bunların otomatik bir teorem ispatlayıcı kullanılarak kanıtlanması (veya çürütülmesi) yoluyla analiz edilebilir. Çalışmamızda biçimsel tanımlama dili olarak Metaslang ve yazılımın kategori teorisine dayalı cebirsel tanımlamasını destekleyen bir araç olan Specware kullandık. Bilgi füzyonundaki en önemli yönlerden biri, belirsiz kaynaklara dayanan füzyon kararlarının belirsizliğidir. Birçok olası belirsizlik türü arasından biz bulanık küme teorisine odaklandık. Bulanık küme teorisinin bir kütüphanesini tanımladık ve bu kütüphane bulanık bilgi işleme sistemlerinin tanımlarını oluşturmak için kullanılabilir. Bir örnek olarak, bir (bulanık) kenar algılama algoritması gerçekleştirildi ve daha sonra iki teorem ispatlayıcı – Snark ve Isabelle – kullanılarak doğrulandı. Bu yaklaşımın yardımıyla, girdi bilgisinin belirsizliğinin füzyon sürecinin her adımındaki etkisi biçimsel olarak tanımlanır ve sistem bir programlama dilinde kodlanmadan önce doğrulanabilir.
Özet (Çeviri)
This thesis explores how an information fusion system can be verified before it is built. Towards this aim, a system is first specified mathematically in a for- mal language. The specification then can be analyzed by formulating various conjectures (theorems) and proving (or disproving) them using an automatic theorem prover. In our work we use Metaslang as the formal specification language and Specware, which is a tool that supports category theory based algebraic specification of software. One of the most important aspects in in- formation fusion is the uncertainty of the fused decisions that are based on uncertain sources. Out of many possible uncertainty types we focus on fuzzy set theory. We have specified a library of fuzzy set theory that can be used to build specifications of fuzzy information processing systems. As an example, a (fuzzy) edge detection algorithm was implemented and then verified using two theorem provers - Snark and Isabelle. With the help of this approach, reasoning about the impact of the uncertainty of input information is speci- fied formally in every step of the fusion process and can be verified before the system is coded in a programming language.
Benzer Tezler
- FPFM: A formal specification and verification framework for security policies in multi-domain mobile networks
FPFM: Çok etki alanlı gezgin ağlarda güvenlik politikaları betimleme ve doğrulama çerçevesi
DEVRİM ÜNAL
Doktora
İngilizce
2011
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET UFUK ÇAĞLAYAN
- Model checking of ambient calculus specifications against ambient logic formulas
Çevrel cebir tanımlamalarının çevrel mantık formülleri ile model denetlemesi
OZAN AKAR
Yüksek Lisans
İngilizce
2009
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET UFUK ÇAĞLAYAN
- Verification and validation of robotic systems's safety
Robotik sistemlerin emniyetinin doğrulanması ve onaylanması
ZEKERİYYA DEMİRCİ
Yüksek Lisans
Türkçe
2023
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolEskişehir Osmangazi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. AHMET YAZICI
DOÇ. DR. METİN ÖZKAN
- Formal verification and controller synthesis for discrete-time systems
Başlık çevirisi yok
EBRU AYDIN GÖL
Doktora
İngilizce
2014
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoston UniversityPROF. CALIN BELTA
- Anklaşman sistemi yazılım modelinin model sınamasının yapılması
Model verification of interlocking software model
DAVUT POLAT
Yüksek Lisans
Türkçe
2015
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. TOLGA OVATMAN