Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/21465
Full metadata record
| DC Field | Value | Language |
|---|---|---|
| dc.contributor.advisor | พรศิริ หมื่นไชยศรี | - |
| dc.contributor.author | นนทศักดิ์ จันทร์ชุม | - |
| dc.contributor.other | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ | - |
| dc.date.accessioned | 2012-08-16T14:23:15Z | - |
| dc.date.available | 2012-08-16T14:23:15Z | - |
| dc.date.issued | 2551 | - |
| dc.identifier.uri | http://cuir.car.chula.ac.th/handle/123456789/21465 | - |
| dc.description | วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2551 | en |
| dc.description.abstract | วิทยานิพนธ์นี้มีวัตถุประสงค์เพื่อนำเสนอวิธีการสำหรับการทวนสอบสมบัตินำเข้า/นำออกของแบบจำลองประกอบด้วยการตรวจสอบแบบจำลอง แบบจำลองประกอบในวิทยานิพนธ์นี้ได้รับจากการประกอบแบบจำลองบนพื้นฐานของกระแสเฉพาะรายด้วยตัวดำเนินการประกอบแบบลำดับ ด้วยตัวดำเนินการประกอบแบบลำดับนี้แบบจำลองประกอบสามารถจำลองด้วยฟังก์ชันการประมวลผลกระแส ฟังก์ชันการประมวลผลกระแสสามารถแปลงเป็นระบบเปลี่ยนสถานะนำเข้า/นำออกที่เป็นแบบจำลองบนพื้นฐานสถานะที่มีความเหมาะสมสำหรับการทวนสอบสมบัตินำเข้า/นำออกที่คาดหมายด้วยการตรวจสอบแบบจำลอง ฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองประกอบสามารถพิจารณาได้จากฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองบนพื้นฐานของกระแสเฉพาะรายที่นำมาประกอบ และสมบัตินำเข้า/นำออกที่คาดหมายของแบบจำลองประกอบซึ่งได้จากการเปลี่ยนนำออกของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบแรกโดยการประยุกต์ฟังก์ชันการประมวลผลกระแสของส่วนประกอบที่สองไปยังนำออกของส่วนประกอบแรก และเปลี่ยนนำเข้าของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบที่สอง โดยการประยุกต์ผกผันของฟังก์ชันการประมวลผลกระแสของส่วนประกอบแรก (ถ้ามี) ไปยังนำเข้าของส่วนประกอบที่สอง | en |
| dc.description.abstractalternative | 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. | en |
| dc.format.extent | 1511150 bytes | - |
| dc.format.mimetype | application/pdf | - |
| dc.language.iso | th | es |
| dc.publisher | จุฬาลงกรณ์มหาวิทยาลัย | en |
| dc.relation.uri | http://doi.org/10.14457/CU.the.2008.1324 | - |
| dc.rights | จุฬาลงกรณ์มหาวิทยาลัย | en |
| dc.subject | พีชคณิตนามธรรม | en |
| dc.subject | แบบจำลองทางคณิตศาสตร์ | en |
| dc.title | การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ | en |
| dc.title.alternative | Functional verification for composite model of stream-based design on history abstraction | en |
| dc.type | Thesis | es |
| dc.degree.name | วิทยาศาสตรมหาบัณฑิต | es |
| dc.degree.level | ปริญญาโท | es |
| dc.degree.discipline | วิทยาศาสตร์คอมพิวเตอร์ | es |
| dc.degree.grantor | จุฬาลงกรณ์มหาวิทยาลัย | en |
| dc.email.advisor | Pornsiri.m@chula.ac.th | - |
| dc.identifier.DOI | 10.14457/CU.the.2008.1324 | - |
| Appears in Collections: | Eng - Theses | |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| Nontasak_ja.pdf | 1.48 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.