Tag LTL

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

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