The Use of a theorem prover to verify a liquid flow control program
Bir teorem ispatlayıcısının bir sıvı akış kontrol programını doğrulamada kullanımı
- Tez No: 29945
- Danışmanlar: DOÇ.DR. VAROL AKMAN
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Program Doğrulama, Boyer-Moore Teorem Ispatlayıcısı (NQTHM), Gerçek- Zamanlı Kontrol, Benzetim, Sağduyusal Akıl Yürütme, Sıvılar iv, Program Verification, Boyer-Moore Theorem Prover (NQTHM), Real-Time Control, Simulation, Commonsense Reasoning, Liquids m
- Yıl: 1993
- Dil: İngilizce
- Üniversite: İhsan Doğramacı Bilkent Üniversitesi
- Enstitü: Mühendislik ve Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Belirtilmemiş.
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 63
Özet
ÖZET BİR TEOREM İSPATLAYICININ BİR SIVI AKIŞ KONTROL PROGRAMINI DO?RULAMADA KULLANILMASI Erkan Uçar Bilgisayar ve Enformatik Mühendisliği, Yüksek Lisans Danışman: Doç. Dr. Varol Akman Şubat, 1993 Güvenilir yazılım ürettiğinden dolayı program doğrulama önemli bir iştir. Uygulamalarının gerçek dünyada çalıştırılmasından ötürü gerçek-zamanlı kon trol programlarının doğrulanması özel dikkat ister ve bunların matematiksel özelliklerini bulmak zordur. Ayrıca, büyük gerçek-zamanlı programlan elle doğrulamak imkansızdır. Bu nedenlerden dolayı, mekanik program doğrulama sistemleri kullanılması gerekir. Aslında genel-amaçlı bir otomatik teorem is- patlayıcı olan Boyer-Moore Teorem Ispatlayıcısı (NQTHM) böyle bir sistemdir. Biz NQTHM'i kullanarak basit bir gerçek-zamanlı sistemin, yani bir su-tank kompleksinin, kontrol programlarını doğruladık. Bu amaca yönelik olarak WA TERWORKS isimli kullanışlı bir benzetim sistemi gerçekleştirdik.
Özet (Çeviri)
ABSTRACT THE USE OF A THEOREM PROVER TO VERIFY A LIQUID FLOW CONTROL PROGRAM Erkan Uçar M.S. in Computer Engineering and Information Science Advisor: Assoc. Prof. Varol Akman February, 1993 Program verification is an important task since it produces reliable software. Verification of real-time control programs needs special attention since these run in the real world and it is difficult to determine their mathematical prop erties. Besides, validating large real-time programs manually is impossible. Owing to these reasons, mechanical program verification systems have to be used. Boyer-Moore Theorem Prover (NQTHM) which, in fact, is a general- purpose automated theorem prover, is such a system. We corroborated the control programs of a simple real-time system, viz. a water-tank complex, using NQTHM. A useful simulator (called WATERWORKS) has been imple mented for this purpose.
Benzer Tezler
- Generating libraries of highly correct and safe functions by using proof-based formal methods
İspat-tabanlı yazılım doğruluğu ve güvenilirliğini gösterme tekniklerini kullanarak güvenilir bir kütüphane oluşturmak
AYUB ROKHMAN WAKHID
Yüksek Lisans
İngilizce
2014
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolMelikşah ÜniversitesiElektrik ve Bilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. AYTEKİN VARGÜN
- How cryptographic implementations affect mobile agent systems
Şifreleme gerçekleştirmelerinin gezgin aracı internet sistemlerini nasıl etkilediği
İSMAİL ULUKUŞ
Yüksek Lisans
İngilizce
2003
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiSistem ve Kontrol Mühendisliği Ana Bilim Dalı
PROF. DR. EMİN ANARIM
- RSA algoritmasını kullanan şifreleme/deşifreleme yazılımının tasarımı
Data encyption/decryption methods and software design of RSA algorithm
METİN ERHAN
Yüksek Lisans
Türkçe
1993
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiDOÇ.DR. BÜLENT ÖRENCİK
- A backwards theorem prover with focusing, resource management and constraints for robotic planning within intuitionistic linear logic
Robotik planlama için odaklanma, kaynak yönetimi ve kısıtlamaların katılarak hedefe yönelik teorem ispatlamanın sezgisel doğrusal mantıkta gerçekleştirimi
SITAR KORTİK
Yüksek Lisans
İngilizce
2010
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİhsan Doğramacı Bilkent ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. ULUÇ SARANLI
- Linear planning logic and linear logic graph planner: Domain independent task planners based on linear logic
Doğrusal planlama mantığı ve doğrusal mantık grafik planlayıcı: Doğrusal mantık tabanlı alan bağımsız görev planlayıcılar
SITAR KORTİK
Doktora
İngilizce
2017
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİhsan Doğramacı Bilkent ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. VAROL AKMAN