ชื่อบทความที่เผยแพร่ |
Transforming of the Sequence Diagram into
Time-Automata Network |
วัน/เดือน/ปี ที่เผยแพร่ |
7 กรกฎาคม 2566 |
การประชุม |
ชื่อการประชุม |
The 29th International MultiConference of Engineers and Computer Scientists (IMECS 2023) |
หน่วยงาน/องค์กรที่จัดประชุม |
International Association of Engineers (IAENG) |
สถานที่จัดประชุม |
Hong Kong |
จังหวัด/รัฐ |
|
ช่วงวันที่จัดประชุม |
5 กรกฎาคม 2566 |
ถึง |
7 กรกฎาคม 2566 |
Proceeding Paper |
Volume (ปีที่) |
2023 |
Issue (เล่มที่) |
1 |
หน้าที่พิมพ์ |
147-152 |
Editors/edition/publisher |
|
บทคัดย่อ |
Formal verification using a model checking
approach is a process for proving undesirable properties in
designed models. The model checking procedure for the
sequence diagram is cumbersome because the transformation of
the sequence diagram into a formal model requires meticulous
mapping rules and methods that must yield corresponding
behaviors. This paper proposes the transformation of the
sequence diagram into a time automate named UPPAAL. The
obtained time automata model can be used to verify deadlock,
undesirable properties, and the correctness of message ordering.
The transformation rules and framework were experimented
with case studies. The results show that the proposed
transformation rules can be applied and map the sequence
diagram into a UPPAL structure correctly. |
ผู้เขียน |
|
การประเมินบทความ (Peer Review) |
มีผู้ประเมินอิสระ |
มีการเผยแพร่ในระดับ |
นานาชาติ |
รูปแบบ Proceeding |
Full paper |
รูปแบบการนำเสนอ |
Oral |
เป็นส่วนหนึ่งของวิทยานิพนธ์ |
เป็น |
ผลงานที่นำเสนอได้รับรางวัล |
ไม่ได้รับรางวัล |
แนบไฟล์ |
|
Citation |
0
|
|