Chulalongkorn University Theses and Dissertations (Chula ETD)
การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ
Other Title (Parallel Title in Other Language of ETD)
Functional verification for composite model of stream-based design on history abstraction
Year (A.D.)
2008
Document Type
Thesis
First Advisor
พรศิริ หมื่นไชยศรี
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Degree Name
วิทยาศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิทยาศาสตร์คอมพิวเตอร์
DOI
10.58837/CHULA.THE.2008.1252
Abstract
วิทยานิพนธ์นี้มีวัตถุประสงค์เพื่อนำเสนอวิธีการสำหรับการทวนสอบสมบัตินำเข้า/นำออกของแบบจำลองประกอบด้วยการตรวจสอบแบบจำลอง แบบจำลองประกอบในวิทยานิพนธ์นี้ได้รับจากการประกอบแบบจำลองบนพื้นฐานของกระแสเฉพาะรายด้วยตัวดำเนินการประกอบแบบลำดับ ด้วยตัวดำเนินการประกอบแบบลำดับนี้แบบจำลองประกอบสามารถจำลองด้วยฟังก์ชันการประมวลผลกระแส ฟังก์ชันการประมวลผลกระแสสามารถแปลงเป็นระบบเปลี่ยนสถานะนำเข้า/นำออกที่เป็นแบบจำลองบนพื้นฐานสถานะที่มีความเหมาะสมสำหรับการทวนสอบสมบัตินำเข้า/นำออกที่คาดหมายด้วยการตรวจสอบแบบจำลอง ฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองประกอบสามารถพิจารณาได้จากฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองบนพื้นฐานของกระแสเฉพาะรายที่นำมาประกอบ และสมบัตินำเข้า/นำออกที่คาดหมายของแบบจำลองประกอบซึ่งได้จากการเปลี่ยนนำออกของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบแรกโดยการประยุกต์ฟังก์ชันการประมวลผลกระแสของส่วนประกอบที่สองไปยังนำออกของส่วนประกอบแรก และเปลี่ยนนำเข้าของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบที่สอง โดยการประยุกต์ผกผันของฟังก์ชันการประมวลผลกระแสของส่วนประกอบแรก (ถ้ามี) ไปยังนำเข้าของส่วนประกอบที่สอง
Other Abstract (Other language abstract of ETD)
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.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
จันทร์ชุม, นนทศักดิ์, "การทวนสอบเชิงฟังก์ชันสำหรับแบบจำลองประกอบของการออกแบบบนพื้นฐานของกระแสด้วยภาวะนามธรรมประวัติ" (2008). Chulalongkorn University Theses and Dissertations (Chula ETD). 67113.
https://digital.car.chula.ac.th/chulaetd/67113