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

Formal Verification of Automotive Software

אימות פורמלי (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.

G. Katz, C. Barrett, D. Dill, K. Julian and M. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.Proc. 29th Int. Conf. on Computer Aided Verification (CAV). Heidelberg, Germany, July 2017. To appear. 

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.