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