אימות פורמלי של רכיב תוכנה למערכות נהיגה אוטומטיות

Formal Verification of software for autonomous vehicle control

תיאור הפרויקט ותכולתו:

אימות פורמלי (Formal Verification)  מאפשר שימוש באלגוריתמים ושיטות מתמטיות להוכחת נכונות של מערכות תוכנה וחומרה מורכבות. מערכות נהיגה אוטומטיות נדרשות לעמוד באתגרים רבים כדי להבטיח נהיגה אמינה ובטוחה, כאשר כל שגיאה במערכות התוכנה עשויה להיות בעלת השלכות משמעותיות על בטיחות הנוסעים. בפרויקט נתמקד במידול רכיב תוכנה של מערכת נהיגה אוטומטית ואימות ההתנהגות שנדרשת מרכיב זה.

במהלך הפרויקט הסטודנטים ירכשו ידע באימות פורמלי    (Formal Verification)    ויישמו אותו באמצעות תיאור של רכיב תוכנה של מערכת נהיגה אוטומטית, הגדרת דרישות בטיחות ותגובתיות של המערכת ושימוש בכלי אימות להוכחת נכונות התכונות וזיהוי כשלים אפשריים. 

דרישות:

83691 Formal Verification and Synthesis (במקביל לפרויקט)

מקורות:

Althoff, Matthias, et al. "Safety verification of autonomous vehicles for coordinated evasive maneuvers." Intelligent vehicles symposium (IV), 2010 IEEE. IEEE, 2010.

Loos, Sarah M., André Platzer, and Ligia Nistor. "Adaptive cruise control: Hybrid, distributed, and now formally verified." FM 2011: Formal Methods. Springer Berlin Heidelberg, 2011. 42-56.

Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).

Nilsson, Petter, et al. "Preliminary results on correct-by-construction control software synthesis for adaptive cruise control." Decision and Control (CDC), 2014 IEEE 53rd Annual Conference on. IEEE, 2014.

email: hillelk@biu.ac.il