การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ

นนทศักดิ์ จันทร์ชุม

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

Title:	การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ
Other Titles:	Functional verification for composite model of stream-based design on history abstraction
Authors:	นนทศักดิ์ จันทร์ชุม
Advisors:	พรศิริ หมื่นไชยศรี
Other author:	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์
Advisor's Email:	Pornsiri.m@chula.ac.th
Subjects:	พีชคณิตนามธรรม แบบจำลองทางคณิตศาสตร์
Issue Date:	2551
Publisher:	จุฬาลงกรณ์มหาวิทยาลัย
Abstract:	วิทยานิพนธ์นี้มีวัตถุประสงค์เพื่อนำเสนอวิธีการสำหรับการทวนสอบสมบัตินำเข้า/นำออกของแบบจำลองประกอบด้วยการตรวจสอบแบบจำลอง แบบจำลองประกอบในวิทยานิพนธ์นี้ได้รับจากการประกอบแบบจำลองบนพื้นฐานของกระแสเฉพาะรายด้วยตัวดำเนินการประกอบแบบลำดับ ด้วยตัวดำเนินการประกอบแบบลำดับนี้แบบจำลองประกอบสามารถจำลองด้วยฟังก์ชันการประมวลผลกระแส ฟังก์ชันการประมวลผลกระแสสามารถแปลงเป็นระบบเปลี่ยนสถานะนำเข้า/นำออกที่เป็นแบบจำลองบนพื้นฐานสถานะที่มีความเหมาะสมสำหรับการทวนสอบสมบัตินำเข้า/นำออกที่คาดหมายด้วยการตรวจสอบแบบจำลอง ฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองประกอบสามารถพิจารณาได้จากฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองบนพื้นฐานของกระแสเฉพาะรายที่นำมาประกอบ และสมบัตินำเข้า/นำออกที่คาดหมายของแบบจำลองประกอบซึ่งได้จากการเปลี่ยนนำออกของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบแรกโดยการประยุกต์ฟังก์ชันการประมวลผลกระแสของส่วนประกอบที่สองไปยังนำออกของส่วนประกอบแรก และเปลี่ยนนำเข้าของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบที่สอง โดยการประยุกต์ผกผันของฟังก์ชันการประมวลผลกระแสของส่วนประกอบแรก (ถ้ามี) ไปยังนำเข้าของส่วนประกอบที่สอง
Other Abstract:	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.
Description:	วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2551
Degree Name:	วิทยาศาสตรมหาบัณฑิต
Degree Level:	ปริญญาโท
Degree Discipline:	วิทยาศาสตร์คอมพิวเตอร์
URI:	http://cuir.car.chula.ac.th/handle/123456789/21465
URI:	http://doi.org/10.14457/CU.the.2008.1324
metadata.dc.identifier.DOI:	10.14457/CU.the.2008.1324
Type:	Thesis
Appears in Collections:	Eng - Theses

Files in This Item:

File	Description	Size	Format
Nontasak_ja.pdf		1.48 MB	Adobe PDF	View/Open

Show full item record