วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2544

วิทยานิพนธ์นี้เสนอวิธีการใหม่ในการกำหนดรูปนัยโพรโทคอลทีซีพีด้วยภาษาคาเฟ่โอบีเจ โดยใช้แผนภาพเอดีเจ และแผนภาพการเปลี่ยนสถานะ ในการเขียนข้อกำหนดโพรโทคอลพีซีพี วิธีการจัดรูปนัยใหม่นี้สามารถกำหนดหลักนามธรรมข้อมูลของโพรโทคอลทีซีพีด้วยแผนภาพเอดีเจ และสามารถแสดงกระบวนการทำงานของทีซีพีได้จากแผนภาพการเปลี่ยนสถานะ อีกทั้งมีการใช้แผนภาพเส้นกำหนดเวลาเพื่อแสดงถึงการรับและส่งข้อมูลระหว่างทีซีพี รวมไปถึงกฎการเชื่อมแผนภาพและเอดีเจ แผนภาพการเปลี่ยนสถานะ และแผนภาพเส้นกำหนดเวลาเข้าด้วยกัน ข้อกำหนดโพรโทคอลทีซีพีนี้ยึดมาตรฐานตามอาร์เอฟซี793 โดยที่ข้อกำหนดไม่ครอบคลุมกรณีที่ผิดพลาด กรณีมีตัวชี้บ่งการเร่ง และกรณีหมดเวลา ซึ่งวิธีรูปนัยศึกษากรณีการ-ติดตั้งการเชื่อมต่อ การรับส่งข้อมูลและการยกเลิกการติดต่อ รวมไปถึงข้อกำหนดของระบบการ-เรียกใช้งานจากผู้ใช้ผ่านคำสั่งเรียกไปยังโพรโทคอลทีซีพีข้อกำหนดดังกล่าวกำหนดและทวนสอบด้วยภาษาคาเฟ่โอบีเจ ซึ่งผลลัพธ์ได้รับการตรวจสอบในส่วนวากยสัมพันธ์และการพิสูจน์ทางคณิตศาสตร์ด้วยภาษาคาเฟ่โอบีเจเช่นกัน