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, Bilgisayar programları, Denetim sistemleri, Sıvı hareketi, Teorem ispatlayıcı, Yazılım endüstrisi, Program Verification, Boyer-Moore Theorem Prover (NQTHM), Real-Time Control, Simulation, Commonsense Reasoning, Liquids m, Computer programs, Control systems, Program verify, Liquid movement, Theorem prover, Software industry
- 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ı: Belirtilmemiş.
Ö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
- 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
- Sobolev ve logaritmik sobolev eşitsizlikleri
Sobolev and logarithmic sobolev inequalities
FARUK GÜNGÖR
- BRST ve antibrst simetrilerinde genel hayalet dekuple teoremi
A General ghost decoupling theorem using BRST and antibrst symmetries
REYHAN AYDIN
Yüksek Lisans
Türkçe
1990
Fizik ve Fizik Mühendisliğiİstanbul Teknik ÜniversitesiPROF.DR. MAHMUT HORTAÇSU
- Sınır elemanları metodu
Boundary elements method
ERDEM SERKAN SAATÇİOĞLU
Yüksek Lisans
Türkçe
1997
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
PROF. DR. TEOMAN KURTAY
- Yapay zeka uygulamaları
Artificial intelligence applications
PINAR AKKUŞ
Yüksek Lisans
Türkçe
1990
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiDOÇ.DR. MİTHAT UYSAL