การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ
วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2551
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Theses and Dissertations |
| Language: | Thai |
| Published: |
จุฬาลงกรณ์มหาวิทยาลัย
2012
|
| Subjects: | |
| Online Access: | http://cuir.car.chula.ac.th/handle/123456789/21465 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Chulalongkorn University |
| Language: | Thai |
| id |
th-cuir.21465 |
|---|---|
| record_format |
dspace |
| spelling |
th-cuir.214652012-08-16T14:23:16Z การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ Functional verification for composite model of stream-based design on history abstraction นนทศักดิ์ จันทร์ชุม พรศิริ หมื่นไชยศรี จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ พีชคณิตนามธรรม แบบจำลองทางคณิตศาสตร์ วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2551 วิทยานิพนธ์นี้มีวัตถุประสงค์เพื่อนำเสนอวิธีการสำหรับการทวนสอบสมบัตินำเข้า/นำออกของแบบจำลองประกอบด้วยการตรวจสอบแบบจำลอง แบบจำลองประกอบในวิทยานิพนธ์นี้ได้รับจากการประกอบแบบจำลองบนพื้นฐานของกระแสเฉพาะรายด้วยตัวดำเนินการประกอบแบบลำดับ ด้วยตัวดำเนินการประกอบแบบลำดับนี้แบบจำลองประกอบสามารถจำลองด้วยฟังก์ชันการประมวลผลกระแส ฟังก์ชันการประมวลผลกระแสสามารถแปลงเป็นระบบเปลี่ยนสถานะนำเข้า/นำออกที่เป็นแบบจำลองบนพื้นฐานสถานะที่มีความเหมาะสมสำหรับการทวนสอบสมบัตินำเข้า/นำออกที่คาดหมายด้วยการตรวจสอบแบบจำลอง ฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองประกอบสามารถพิจารณาได้จากฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองบนพื้นฐานของกระแสเฉพาะรายที่นำมาประกอบ และสมบัตินำเข้า/นำออกที่คาดหมายของแบบจำลองประกอบซึ่งได้จากการเปลี่ยนนำออกของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบแรกโดยการประยุกต์ฟังก์ชันการประมวลผลกระแสของส่วนประกอบที่สองไปยังนำออกของส่วนประกอบแรก และเปลี่ยนนำเข้าของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบที่สอง โดยการประยุกต์ผกผันของฟังก์ชันการประมวลผลกระแสของส่วนประกอบแรก (ถ้ามี) ไปยังนำเข้าของส่วนประกอบที่สอง The objective of this thesis is to present a method for verifying input/output properties of a composite model with model checking. The composite model in this thesis is derived from composing individual stream-based models with a sequential composition operator. With the sequential composition operator, composite model can be modeled with a stream processing function. The stream processing function can be transformed into an input/output transition systems, a state-based model which is suitable for verifying expected input/output properties with model checking. A history abstraction for the Moore machine, which is a state-based model for implementation, plays a crucial role in reducing the number of states of an input/output transition system. With a finite state space, a stream processing function is used to verified input/output properties with model checking. A history abstraction for the Moore machine of a composite model can be considered from history abstractions for the Moore machine of individual stream-based models. Expected input/output properties of a composite model can be obtained from changing output of expected input/output properties of the first component by applying the stream processing function of the second component to output of the first component and/or changing input of expected input/output properties of the second component by applying the inverse stream processing function of the first component (if exists) to input of the second component. 2012-08-16T14:23:15Z 2012-08-16T14:23:15Z 2551 Thesis http://cuir.car.chula.ac.th/handle/123456789/21465 th จุฬาลงกรณ์มหาวิทยาลัย 1511150 bytes application/pdf application/pdf จุฬาลงกรณ์มหาวิทยาลัย |
| institution |
Chulalongkorn University |
| building |
Chulalongkorn University Library |
| country |
Thailand |
| collection |
Chulalongkorn University Intellectual Repository |
| language |
Thai |
| topic |
พีชคณิตนามธรรม แบบจำลองทางคณิตศาสตร์ |
| spellingShingle |
พีชคณิตนามธรรม แบบจำลองทางคณิตศาสตร์ นนทศักดิ์ จันทร์ชุม การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ |
| description |
วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2551 |
| author2 |
พรศิริ หมื่นไชยศรี |
| author_facet |
พรศิริ หมื่นไชยศรี นนทศักดิ์ จันทร์ชุม |
| format |
Theses and Dissertations |
| author |
นนทศักดิ์ จันทร์ชุม |
| author_sort |
นนทศักดิ์ จันทร์ชุม |
| title |
การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ |
| title_short |
การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ |
| title_full |
การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ |
| title_fullStr |
การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ |
| title_full_unstemmed |
การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ |
| title_sort |
การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ |
| publisher |
จุฬาลงกรณ์มหาวิทยาลัย |
| publishDate |
2012 |
| url |
http://cuir.car.chula.ac.th/handle/123456789/21465 |
| _version_ |
1681410293894217728 |