The Use of a theorem prover to verify a liquid flow control program

Abstract

Ö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. Anahtar Sözcükler: 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

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. Keywords: Program Verification, Boyer-Moore Theorem Prover (NQTHM), Real-Time Control, Simulation, Commonsense Reasoning, Liquids m