5 שאלות לפרופ' אמיר פנואלי

 

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

 

כדי למנוע את התרחשותן של תקלות מסוג זה, אפשר לנסות לבדוק את המערכות בשורה ארוכה של הדמיות מצב (סימולציות). אבל בדיקות מסוג זה (משוכללות ככל שיהיו), עדיין מותירות אפשרות ש"תסריטים" מסוימים נותרו מחוץ לטווח הבדיקה; ודווקא מקרים אלה (גם אם הסבירות להתרחשותם קטנה), עלולים בכל זאת להתרחש, דבר שעלול להוביל לתקלות קטלניות.

 

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

 

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

 

"לוגיקת זמן היא שפה מתמטית, שבה אפשר לנסח ולהוכיח משפטים שטוענים טענות הקשורות גם בממד הזמן. לדוגמא: "עכשיו המציאות היא כזאת, והעובדות האלה נכונות, אבל מחר המציאות תשתנה, ויחד אתה ישתנו גם העובדות".

 

"תוך כדי עבודה התברר לי, שהתכונה המאפיינת את המערכות הממוחשבות שלוגיקת הזמן מתאימה במיוחד לאימותן, היא ה'תגובתיות' שלהן. כלומר: מידת יכולתן להגיב לאירועים חיצוניים, בזמן.

 

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

 

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

 

האיחוד האירופי, למשל, מבצע כיום פרויקט גדול שתכליתו פיתוח דרכים אחידות לאימות מערכות, ממוחשבות מפני שכל תקלה בהן עלולה לגרום, שורת נזקים כבדים".