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

• Main Author: นนทศักดิ์ จันทร์ชุม
• Other Authors: พรศิริ หมื่นไชยศรี
• Format: Theses and Dissertations
• Language: Thai
• Published: จุฬาลงกรณ์มหาวิทยาลัย 2008
• Subjects: พีชคณิตนามธรรม; แบบจำลองทางคณิตศาสตร์
• Online Access: https://digiverse.chula.ac.th/Info/item/dc:44256
• Institution: Chulalongkorn University

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.