Chulalongkorn University Theses and Dissertations (Chula ETD)
Conformance verification of finite state machines based on machine inference and model checking
Other Title (Parallel Title in Other Language of ETD)
การทวนสอบความสอดคล้องของเครื่องจักรสถานะจำกัดโดยการอนุมานเครื่องและการตรวจสอบโมเดล
Year (A.D.)
2012
Document Type
Thesis
First Advisor
Athasit Surarerks
Second Advisor
Pattarasinee Bhattarakosol
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Degree Name
Doctor of Engineering
Degree Level
Doctoral Degree
Degree Discipline
Computer Engineering
DOI
10.58837/CHULA.THE.2012.1384
Abstract
The conformance problem has attracted much interest in the research field of software verification, since the implementation that doesn’t conform to the specification may cause some errors such as the communicating interruption in the composited application. However, the earlier works in conformance verification assume that the internal structures of the implementation are explicit. It may not always be the case such as the applications that implemented in .NET or Java. In this dissertation, we propose an alternative approach for verifying a conformance between the specification and the implementation whose only external behaviors can be observed. We use an adapted version of Angluin’s algorithm to infer a deterministic Finite State Machine (FSM) from the implementations. By transforming the obtained model to the modeling formalism LTS, the model checker LTSA can be used for checking the conformance criterion in our framework. From the experiment based on Web services composition, we can detect the execution trace of the implemented Web service that does not conform to the choreography specification. Moreover, since the assumption that the implementations have to be deterministic may be too restricted in some applications (such as, a communication system or a component-based system), we also present a novel learning algorithm, namely|which can be applied to infer both deterministic and non-deterministic FSMs.
Other Abstract (Other language abstract of ETD)
ปัญหาความสอดคล้องได้รับความสนใจอย่างมากในงานวิจัยทางด้านการทวนสอบซอฟต์แวร์ เนื่องจากซอฟต์แวร์ที่ไม่สามารถทำงานได้ตรงตามที่ระบุไว้ในข้อกำหนดซอฟต์แวร์อาจทำให้เกิดปัญหาต่างๆ เช่น การหยุดชะงักในระหว่างการสื่อสารกับซอฟต์แวร์อื่น แต่สมมติฐานเบื้องต้นในงานวิจัยด้านการทวนสอบความสอดคล้องในปัจจุบัน คือ เราสามารถมองเห็นโครงสร้างภายในของซอฟต์แวร์ที่จะนำมาทวนสอบได้ ข้อจำกัดดังกล่าวทำให้เราไม่สามารถทวนสอบซอฟต์แวร์บางประเภท เช่น ซอฟต์แวร์ที่พัฒนาด้วยภาษา .NET หรือ Java ได้ เนื่องจากไม่สามารถมองเห็นการทำงานภายในได้ ในวิทยานิพนธ์นี้ผู้วิจัยได้เสนอวิธีการใหม่ในการทวนสอบความสอดคล้องของข้อกำหนดซอฟต์แวร์กับซอฟต์แวร์ที่สามารถมองเห็นได้แต่พฤติกรรมภายนอก โดยผู้วิจัยใช้ขั้นตอนวิธีในการอนุมานเครื่องเพื่อให้ได้เครื่องจักรสถานะจำกัดจากซอฟต์แวร์ที่ไม่สามารถมองเห็นโครงสร้างภายในได้ หลังจากได้เครื่องจักรสถานะจำกัดของซอฟต์แวร์จากขั้นตอนวิธีดังกล่าวแล้วจึงนำไปแปลงเป็นภาษารูปนัย LTS เพื่อใช้การตรวจสอบโมเดล LTSA ตรวจสอบความสอดคล้องของโมเดลที่ได้และโมเดลของข้อกำหนดซอฟต์แวร์ต่อไป จากผลการทดลองกับการประกอบเว็บเซอร์วิสผู้วิจัยสามารถตรวจพบการทำงานของเว็บเซอร์วิสที่ไม่ตรงตามที่ระบุไว้ในข้อกำหนดซอฟต์แวร์ได้ และเนื่องจากขั้นตอนวิธีที่นำมาใช้สามารถอนุมานเครื่องจักรสถานะจำกัดเชิงกำหนดได้เพียงอย่างเดียว ผู้วิจัยจึงได้เสนอขั้นตอนวิธี ที่สามารถอนุมานได้ทั้งเครื่องจักรสถานะจำกัดเชิงกำหนดและเชิงไม่กำหนด
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
Pacharoen, Warawoot, "Conformance verification of finite state machines based on machine inference and model checking" (2012). Chulalongkorn University Theses and Dissertations (Chula ETD). 68897.
https://digital.car.chula.ac.th/chulaetd/68897