 |
| ภาพจาก Columbia Engineering News |
เครื่องมือ Spoq ที่พัฒนาโดยนักวิจัย Software Systems Laboratory (SSL) ของ Columbia University ช่วยลดความยุ่งยากในการทวนสอบ (verification) ซอฟต์แวร์ระบบอย่างเป็นทางการ และช่วยให้สามารถยืนยันโค้ดของโปรแกรมระบบที่เขียนด้วยภาษา C ที่มีอยู่ได้โดยไม่ต้องแก้ไข
การทวนสอบระบบอย่างเป็นทางการแสดงให้เห็นถึงความปลอดภัยของซอฟต์แวร์ในทุกสถานการณ์ในรูปแบบคณิตศาสตร์
Spoq ได้รับการออกแบบมาเพื่อลดความพยายามในการทวนสอบด้วยตนเองที่น่าเบื่อโดยทำให้การทวนสอบอย่างเป็นทางการหลายแง่มุมเป็นแบบอัตโนมัติ
Xupeng Li จากโคลัมเบียกล่าวว่า "Spoq สามารถสร้างผลลัพธ์ได้ภายในเวลาประมาณหนึ่งชั่วโมง เมื่อเทียบกับการทำด้วยตนเอง ซึ่งอาจต้องใช้เวลาหลายเดือนหรือหลายปีในการทวนสอบระบบอย่างเป็นทางการ"
SSL ตั้งใจที่จะเปิด Spoq ให้เป็นแบบโอเพ่นซอร์สในอีกไม่กี่เดือนข้างหน้าเพื่อให้การทวนสอบอย่างเป็นทางการเกิดขึ้นในวงกว้าง
อ่านข่าวเต็มได้ที่: Columbia Engineering News
ไม่มีความคิดเห็น:
แสดงความคิดเห็น