Bir teorem ispatlayıcısının bir sıvı akış kontrol programını doğrulamada kullanımı

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