Geri Dön

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ı

PDF İndir

  1. Tez No: 29945
  2. Yazar: ERKAN UÇAR
  3. Danışmanlar: DOÇ.DR. VAROL AKMAN
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. 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
  7. Yıl: 1993
  8. Dil: İngilizce
  9. Üniversite: İhsan Doğramacı Bilkent Üniversitesi
  10. Enstitü: Mühendislik ve Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Belirtilmemiş.
  12. Bilim Dalı: Belirtilmemiş.
  13. 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

  1. Tez No

    374441

    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

    İngilizce

    2014

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolMelikşah Üniversitesi

    Elektrik ve Bilgisayar Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. AYTEKİN VARGÜN

  2. Tez No

    139400

    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

    İngilizce

    2003

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi Üniversitesi

    Sistem ve Kontrol Mühendisliği Ana Bilim Dalı

    PROF. DR. EMİN ANARIM

  3. Tez No

    39281

    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

    Türkçe

    1993

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik Üniversitesi

    DOÇ.DR. BÜLENT ÖRENCİK

  4. Tez No

    255979

    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

    İngilizce

    2010

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİhsan Doğramacı Bilkent Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    YRD. DOÇ. DR. ULUÇ SARANLI

  5. Tez No

    476643

    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

    İngilizce

    2017

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİhsan Doğramacı Bilkent Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    PROF. DR. VAROL AKMAN

Geri Dön