Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/1181
| Title: | การจัดรูปนัยของโพรโทคอลทีซีพีโดยใช้คาเฟ่โอบีเจ |
| Other Titles: | Formalization of the TCP protocol using CafeOBJ |
| Authors: | สุชาดา จุลจันทร์, 2519- |
| Advisors: | วิวัฒน์ วัฒนาวุฒิ |
| Other author: | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ |
| Advisor's Email: | wiwat@chula.ac.th |
| Subjects: | ทีซีพี/ไอพี (โปรโตคอลเครือข่ายคอมพิวเตอร์) วิธีรูปนัย (วิทยาการคอมพิวเตอร์) ซอฟต์แวร์ -- ข้อกำหนด คาเฟโอบีเจ |
| Issue Date: | 2544 |
| Publisher: | จุฬาลงกรณ์มหาวิทยาลัย |
| Abstract: | วิทยานิพนธ์นี้เสนอวิธีการใหม่ในการกำหนดรูปนัยโพรโทคอลทีซีพีด้วยภาษาคาเฟ่โอบีเจ โดยใช้แผนภาพเอดีเจ และแผนภาพการเปลี่ยนสถานะ ในการเขียนข้อกำหนดโพรโทคอลพีซีพี วิธีการจัดรูปนัยใหม่นี้สามารถกำหนดหลักนามธรรมข้อมูลของโพรโทคอลทีซีพีด้วยแผนภาพเอดีเจ และสามารถแสดงกระบวนการทำงานของทีซีพีได้จากแผนภาพการเปลี่ยนสถานะ อีกทั้งมีการใช้แผนภาพเส้นกำหนดเวลาเพื่อแสดงถึงการรับและส่งข้อมูลระหว่างทีซีพี รวมไปถึงกฎการเชื่อมแผนภาพและเอดีเจ แผนภาพการเปลี่ยนสถานะ และแผนภาพเส้นกำหนดเวลาเข้าด้วยกัน ข้อกำหนดโพรโทคอลทีซีพีนี้ยึดมาตรฐานตามอาร์เอฟซี793 โดยที่ข้อกำหนดไม่ครอบคลุมกรณีที่ผิดพลาด กรณีมีตัวชี้บ่งการเร่ง และกรณีหมดเวลา ซึ่งวิธีรูปนัยศึกษากรณีการ-ติดตั้งการเชื่อมต่อ การรับส่งข้อมูลและการยกเลิกการติดต่อ รวมไปถึงข้อกำหนดของระบบการ-เรียกใช้งานจากผู้ใช้ผ่านคำสั่งเรียกไปยังโพรโทคอลทีซีพีข้อกำหนดดังกล่าวกำหนดและทวนสอบด้วยภาษาคาเฟ่โอบีเจ ซึ่งผลลัพธ์ได้รับการตรวจสอบในส่วนวากยสัมพันธ์และการพิสูจน์ทางคณิตศาสตร์ด้วยภาษาคาเฟ่โอบีเจเช่นกัน |
| Other Abstract: | This thesis proposes new formalization of the TCP protocol specification using CafeOBJ formal language. This technique uses the ADJ Diagram and the State Transition Diagram for specifying the complexity and variety services of the TCP Protocol. This new technique can specify both the data abstraction and the system procedure which are important for specifying and verifying complex system. The data abstraction of the TCP protocol is defined by using ADJ Diagram and the procedure of this specification is analyzed by using the State Transition Diagram. In addition, the combination rules of ADJ Diagram and State Transition Diagram are provided. Furthermore, the flow of sending and receiving data between two TCPs illustrate by using Timed Lined Diagram. In the same manner, the combination rules of the ADJ Diagram, State Transition Diagram and Timed Lined Diagram are provided. The connection establishment, data transfer and termination of TCP specification and user calls system specification are specified and verified according to RFC793. Ignorance timeout interval, no urgent and no error are provided. The results show the TCP specification is syntactically verified by using CafeOBJ Interpreter. |
| Description: | วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2544 |
| Degree Name: | วิศวกรรมศาสตรมหาบัณฑิต |
| Degree Level: | ปริญญาโท |
| Degree Discipline: | วิศวกรรมคอมพิวเตอร์ |
| URI: | http://cuir.car.chula.ac.th/handle/123456789/1181 |
| ISBN: | 9740312748 |
| Type: | Thesis |
| Appears in Collections: | Eng - Theses |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| Suchada.pdf | 9.86 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.