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

תוצרת המכון
01.12.1996

שתף

5 שאלות לפרופ' אמיר פנואלי
 
פרופ' אמיר פנואלי מהמחלקה למתמטיקה שימושית ולמדעי המחשב במכון, זכה באחרונה בפרס טיורינג - הפרס החשוב בעולם בתחום מדעי המחשב - לשנת 1996
 
 
1. אתה עוסק בפיתוח שיטות מתוחכמות ל"אימות מערכות ממוחשבות". במה בדיוק מתמקד התחום הזה?
ככל שהמערכות הממוחשבות מתפתחות, הן נעשות מורכבות ומסובכות יותר; וככל שהן מפקחות על תהליכים הרי גורל יותר (לדוגמא, בקרה של כור גרעיני, שילוח טילים לחלל, ניהול מסלול טיסה של מטוס, בקרת ייצור במפעל תעשייתי, פיקוח על מיכשור רפואי בבתי חולים, פיקוח על מערכות תקשורת וכו'), כך גדל הסיכון שתקלה במערכות האלה תגרום נזקים כבדים, ולעיתים גם אובדן של חיי אדם.
 
כדי למנוע את התרחשותן של תקלות מסוג זה, אפשר לנסות לבדוק את המערכות בשורה ארוכה של הדמיות מצב (סימולציות). אבל בדיקות מסוג זה (משוכללות ככל שיהיו), עדיין מותירות אפשרות ש"תסריטים" מסוימים נותרו מחוץ לטווח הבדיקה; ודווקא מקרים אלה (גם אם הסבירות להתרחשותם קטנה), עלולים בכל זאת להתרחש, דבר שעלול להוביל לתקלות קטלניות.
 
"לנוכח מצב העניינים הזה, עולה אפשרות אחרת: לנסות להוכיח ("לאמת") את התוכנה באמצעות הוכחה מתמטית (כפי שמוכיחים משפט מתמטי, גיאומטרי). הוכחה כזאת תבטיח את נכונותה של התוכנית הנבדקת מעבר לכל צל של ספק".
 
2. אילו עבודות זיכו אותך בפרס טיורינג?
"מדובר בפיתוח שיטות תיאורטיות לאימות תוכניות, ובמיוחד תוכניות מקבילות (המבצעות בעת ובעונה אחת חלקים שונים של משימה מסוימת); ותוכניות שמפקחות על מערכות פיסיקליות, דוגמת תוכנת המחשב שמפקחת על ניהול ובקרת הטיסה של מטוס".
 
3. בהודעה על זכייתך בפרס נאמר, כי פיתחת דרכים להשתמש ב"לוגיקת זמן" לאימות מערכות ממוחשבות, וכן לאיפיונן ולהגדרת הדרישות מהמערכות האלה. מהי "לוגיקת זמן"?
"לוגיקת זמן היא שפה מתמטית, שבה אפשר לנסח ולהוכיח משפטים שטוענים טענות הקשורות גם בממד הזמן. לדוגמא: "עכשיו המציאות היא כזאת, והעובדות האלה נכונות, אבל מחר המציאות תשתנה, ויחד אתה ישתנו גם העובדות".
 
4. שמך נקשר גם בהמצאת מושגי מפתח חדשים במדעי המחשב, כמו "תגובתיות" ו"מערכות משולבות". האם תוכל להסביר מה משמעות המושגים האלה?
"תוך כדי עבודה התברר לי, שהתכונה המאפיינת את המערכות הממוחשבות שלוגיקת הזמן מתאימה במיוחד לאימותן, היא ה'תגובתיות' שלהן. כלומר: מידת יכולתן להגיב לאירועים חיצוניים, בזמן.
 
"כדי להבין את מושג ה'מערכות המעורבות', כדאי לזכור שבמשך שנים רבות היה מקובל להפריד בין המרכיבים ה'בדידים' של מערכת (לדוגמא המרכיב השולט בפתיחת וסגירת שסתומים), לבין המרכיבים ה'רציפים' של המערכת (לדוגמה, התהליכים הכימיים והפיסיקליים המתרחשים בה - כגון תהליכים המתחוללים בתוך דודי ייצור). אלא שכידוע, מערכת שמפעילה, למשל, קו ייצור במפעל גדול, כוללת מרכיבים בדידים ורציפים כאחד. בעבודותי מצאתי דרך לשלב את המרכיבים השונים, ולטפל במערכת כולה כבמכלול אחד".
 
5. אילו שימושים נעשים כיום בטכניקות אימות המערכות שפיתחת?
"טכניקות אימות מערכות שמבוססות על לוגיקת זמן מופעלות בשנים האחרונות, הן ככלי מחקר בשירותם של מדעני מחשב מכל העולם, והן לבחינה מעשית ויישומית של מערכות ממוחשבות גדולות ומסובכות במיוחד.
 
האיחוד האירופי, למשל, מבצע כיום פרויקט גדול שתכליתו פיתוח דרכים אחידות לאימות מערכות, ממוחשבות מפני שכל תקלה בהן עלולה לגרום, שורת נזקים כבדים".
 

שתף