[FV] ลองใช้ LTL ใน Promela

ช่วงนี้หลังจากทำ Term Project เกี่ยวกับระบบ Lift ผมเลยอยากจดไว้ก่อนว่าตัวโปรแกรม SPIN GUI ที่เขียนโดยภาษา Promela สามารถทวนสอบ Linear time Temporal Logic(LTL) ได้อย่างไรครับ โดยทำตามขั้นตอน ดังนี้

สิ่งที่ต้องมี

• Promela Code - ที่เขียน Model ที่ต้องการทวนสอบ
• LTL - ชุดคำสั่งที่ให้สำหรับการทวนสอบ ว่า Model เรามีคุณลักษณะที่ต้องการ หรือป่าว

ขั้นตอนการทวนสอบ LTL ใน Spin GUI

• ทำการเขียนคำสั่ง LTL ตัวอย่าง ต้องการตรวจสอบว่าประตูลิฟต์ของช่องที่ 1 ในทุกๆชั้น สามารถเปิดได้ไม่เกิน 1 ตัว หรือปิดทั้งหมด ที่ใช้ <= 1 เพราะ มีกรณีที่ลิฟต์ปิดหมดทุกตัว และลิฟต์เปิดได้ 1 ตัว สามารถเขียนคำสั่ง ได้ ดังนี้

  #define firstElevatorSiloSafedoors  (firstElevatorDoorOpen[0] + firstElevatorDoorOpen[1] + firstElevatorDoorOpen[2] + firstElevatorDoorOpen[3] + firstElevatorDoorOpen[4] + firstElevatorDoorOpen[5] + firstElevatorDoorOpen[6] + firstElevatorDoorOpen[7]<= 1)
  
  ltl { [] firstElevatorSiloSafedoors }

  หมายเหตุ: ในส่วนของการ #define ไม่ต้องใส่ ; ต่อท้าย

• Save Code และกดปุ่ม Syntax Check ดังรูป
  
• หลังจากกดปุ่ม Syntax Check แล้ว Spin ตรวจสอบโปรแกรมที่เขียนขึ้นสร้าง Model และทำกำหนด ID ให้กับ LTL แต่ละตัง ดังรูป
  
• การทวนสอบ LTL ที่เขียนขึ้น ให้ไปที่ Tab Verification
  
• ทำการกำหนดค่า ดังรูป
  
  จุดที่ 1: เลือก Acceptance Cycles
  จุดที่ 2: เลือก Use Claim
  จุดที่ 3: Claim Name เลือก LTL ที่ได้จากการกด Syntax Check ในขั้นตอนที่ 3 จากตัวอย่างที่เลือกมา พบว่าเป็น ltl_0
• กำหนดค่าให้เรียบร้อย จากนั้นกดปุ่ม Run
  
• ถ้าสังเกตุที่ผลลัพธ์ตรง never claim มีการบอกว่าเป็นการทวนสอบ ltl_0
  
• ถ้าเลื่อนลงมาล่างสุดพบผลลัพธ์ของการทวนสอบ ซึ่งถ้ามี Error ระบบแสดง Trail ให้ แต่ถ้าไม่มีอะไรให้ระบบแสดง No errors found -- did you verify all claims? ดังรูป
  
  สำหรับในส่วนนี้มีการบอกข้อมูลอื่นๆ ด้วย เช่น จำนวนหน่วยความจำที่ใช้ จำนวน State ที่สร้างขึ้น และมี State ไหนมีเข้าไม่ได้ถูก Execute เป็นต้น