Tag FV

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

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

[FV] ลงตัว CPN Tools

สำหรับ Blog นี้ หลังจากลอง Spin แบบมืนๆงงๆกันมาแล้ว คราวนี้มาลองลงตัว CPN Tools ซึ่งเป็นเครื่องมือสำหรับจัดการพวก  Petri nets หรือ Colored Petri nets ครับ โดย Tools เป็นการพัฒนาด้วยภาษา Java ครับ มาเริ่มลงโปรแกรมกันดีกว่า ขั้นตอนการลงโปรแกรม Download ตัวโปรแกรมมากันก่อนเลยครับ จาก  สำหรับผมใช้ Windows ครับ กด Next ยาวๆไปครับ ดูรูปได้จาก Gallery ครับ ลองเปิดโปรแกรมดูครับ ถ้าไม่ขึ้นต้องลอง Set JAVA_HOME ครับ…