ridm@nrct.go.th   ระบบคลังข้อมูลงานวิจัยไทย   รายการโปรดที่คุณเลือกไว้

Conformance verification of finite state machines based on machine inference and model checking

หน่วยงาน จุฬาลงกรณ์มหาวิทยาลัย

รายละเอียด

ชื่อเรื่อง : Conformance verification of finite state machines based on machine inference and model checking
นักวิจัย : Warawoot Pacharoen
คำค้น : Computer software -- Quality control , Computer software -- Specifications , ปริญญาดุษฎีบัณฑิต , ซอฟต์แวร์ -- การควบคุมคุณภาพ , ซอฟต์แวร์ -- ข้อกำหนด
หน่วยงาน : จุฬาลงกรณ์มหาวิทยาลัย
ผู้ร่วมงาน : Athasit Surarerks , Pattarasinee Bhattarakosol , Chulalongkorn University. Faculty of Engineering
ปีพิมพ์ : 2555
อ้างอิง : http://cuir.car.chula.ac.th/handle/123456789/36723
ที่มา : -
ความเชี่ยวชาญ : -
ความสัมพันธ์ : -
ขอบเขตของเนื้อหา : -
บทคัดย่อ/คำอธิบาย :

Thesis (Ph.D.)--Chulalongkorn University, 2012

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.

บรรณานุกรม :
Warawoot Pacharoen . (2555). Conformance verification of finite state machines based on machine inference and model checking.
    กรุงเทพมหานคร : จุฬาลงกรณ์มหาวิทยาลัย.
Warawoot Pacharoen . 2555. "Conformance verification of finite state machines based on machine inference and model checking".
    กรุงเทพมหานคร : จุฬาลงกรณ์มหาวิทยาลัย.
Warawoot Pacharoen . "Conformance verification of finite state machines based on machine inference and model checking."
    กรุงเทพมหานคร : จุฬาลงกรณ์มหาวิทยาลัย, 2555. Print.
Warawoot Pacharoen . Conformance verification of finite state machines based on machine inference and model checking. กรุงเทพมหานคร : จุฬาลงกรณ์มหาวิทยาลัย; 2555.