การจัดรูปนัยของโพรโทคอลทีซีพีโดยใช้คาเฟ่โอบีเจ

สุชาดา จุลจันทร์, 2519-

Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/1181

Full metadata record

DC Field	Value	Language
dc.contributor.advisor	วิวัฒน์ วัฒนาวุฒิ	-
dc.contributor.author	สุชาดา จุลจันทร์, 2519-	-
dc.contributor.other	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์	-
dc.date.accessioned	2006-07-28T10:15:36Z	-
dc.date.available	2006-07-28T10:15:36Z	-
dc.date.issued	2544	-
dc.identifier.isbn	9740312748	-
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/1181	-
dc.description	วิทยานิพนธ์ (วศ.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2544	en
dc.description.abstract	วิทยานิพนธ์นี้เสนอวิธีการใหม่ในการกำหนดรูปนัยโพรโทคอลทีซีพีด้วยภาษาคาเฟ่โอบีเจ โดยใช้แผนภาพเอดีเจ และแผนภาพการเปลี่ยนสถานะ ในการเขียนข้อกำหนดโพรโทคอลพีซีพี วิธีการจัดรูปนัยใหม่นี้สามารถกำหนดหลักนามธรรมข้อมูลของโพรโทคอลทีซีพีด้วยแผนภาพเอดีเจ และสามารถแสดงกระบวนการทำงานของทีซีพีได้จากแผนภาพการเปลี่ยนสถานะ อีกทั้งมีการใช้แผนภาพเส้นกำหนดเวลาเพื่อแสดงถึงการรับและส่งข้อมูลระหว่างทีซีพี รวมไปถึงกฎการเชื่อมแผนภาพและเอดีเจ แผนภาพการเปลี่ยนสถานะ และแผนภาพเส้นกำหนดเวลาเข้าด้วยกัน ข้อกำหนดโพรโทคอลทีซีพีนี้ยึดมาตรฐานตามอาร์เอฟซี793 โดยที่ข้อกำหนดไม่ครอบคลุมกรณีที่ผิดพลาด กรณีมีตัวชี้บ่งการเร่ง และกรณีหมดเวลา ซึ่งวิธีรูปนัยศึกษากรณีการ-ติดตั้งการเชื่อมต่อ การรับส่งข้อมูลและการยกเลิกการติดต่อ รวมไปถึงข้อกำหนดของระบบการ-เรียกใช้งานจากผู้ใช้ผ่านคำสั่งเรียกไปยังโพรโทคอลทีซีพีข้อกำหนดดังกล่าวกำหนดและทวนสอบด้วยภาษาคาเฟ่โอบีเจ ซึ่งผลลัพธ์ได้รับการตรวจสอบในส่วนวากยสัมพันธ์และการพิสูจน์ทางคณิตศาสตร์ด้วยภาษาคาเฟ่โอบีเจเช่นกัน	en
dc.description.abstractalternative	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.	en
dc.format.extent	35421741 bytes	-
dc.format.mimetype	application/pdf	-
dc.language.iso	th	en
dc.publisher	จุฬาลงกรณ์มหาวิทยาลัย	en
dc.rights	จุฬาลงกรณ์มหาวิทยาลัย	en
dc.subject	ทีซีพี/ไอพี (โปรโตคอลเครือข่ายคอมพิวเตอร์)	en
dc.subject	วิธีรูปนัย (วิทยาการคอมพิวเตอร์)	en
dc.subject	ซอฟต์แวร์ -- ข้อกำหนด	en
dc.subject	คาเฟโอบีเจ	en
dc.title	การจัดรูปนัยของโพรโทคอลทีซีพีโดยใช้คาเฟ่โอบีเจ	en
dc.title.alternative	Formalization of the TCP protocol using CafeOBJ	en
dc.type	Thesis	en
dc.degree.name	วิศวกรรมศาสตรมหาบัณฑิต	en
dc.degree.level	ปริญญาโท	en
dc.degree.discipline	วิศวกรรมคอมพิวเตอร์	en
dc.degree.grantor	จุฬาลงกรณ์มหาวิทยาลัย	en
dc.email.advisor	wiwat@chula.ac.th	-
Appears in Collections:	Eng - Theses

Files in This Item:

File	Description	Size	Format
Suchada.pdf		9.86 MB	Adobe PDF	View/Open

Show simple item record