วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2551

วิทยานิพนธ์นี้มีวัตถุประสงค์เพื่อนำเสนอวิธีการสำหรับการทวนสอบสมบัตินำเข้า/นำออกของแบบจำลองประกอบด้วยการตรวจสอบแบบจำลอง แบบจำลองประกอบในวิทยานิพนธ์นี้ได้รับจากการประกอบแบบจำลองบนพื้นฐานของกระแสเฉพาะรายด้วยตัวดำเนินการประกอบแบบลำดับ ด้วยตัวดำเนินการประกอบแบบลำดับนี้แบบจำลองประกอบสามารถจำลองด้วยฟังก์ชันการประมวลผลกระแส ฟังก์ชันการประมวลผลกระแสสามารถแปลงเป็นระบบเปลี่ยนสถานะนำเข้า/นำออกที่เป็นแบบจำลองบนพื้นฐานสถานะที่มีความเหมาะสมสำหรับการทวนสอบสมบัตินำเข้า/นำออกที่คาดหมายด้วยการตรวจสอบแบบจำลอง ฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองประกอบสามารถพิจารณาได้จากฟังก์ชันภาวะนามธรรมประวัติสำหรับเครื่องมัวร์ของแบบจำลองบนพื้นฐานของกระแสเฉพาะรายที่นำมาประกอบ และสมบัตินำเข้า/นำออกที่คาดหมายของแบบจำลองประกอบซึ่งได้จากการเปลี่ยนนำออกของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบแรกโดยการประยุกต์ฟังก์ชันการประมวลผลกระแสของส่วนประกอบที่สองไปยังนำออกของส่วนประกอบแรก และเปลี่ยนนำเข้าของสมบัตินำเข้า/นำออกที่คาดหมายของส่วนประกอบที่สอง โดยการประยุกต์ผกผันของฟังก์ชันการประมวลผลกระแสของส่วนประกอบแรก (ถ้ามี) ไปยังนำเข้าของส่วนประกอบที่สอง