מדינת ישראל , משרד החינוך מדינת ישראל , משרד החינוך
מדינת ישראל, משרד החינוך
משרד החינוך
פרסי ישראל

מדינת ישראל,

משרד החינוך

חזרה לרשימה

פרופ' אמיר פנואלי

share
שתפו עמוד:
פרופ' אמיר פנואלי

על הזוכה

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

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

נימוקי השופטים

פרופ' דן שכטמן, יו"ר, פרופ' אברהם בן-ראובן, פרופ' פאול זינגר, פרופ' דן מאירשטיין, פרופ' הלל פורסטנברג

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

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

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

המשמעות היישומית של עבודתו החלוצית הזאת היא אדירה, ואלגוריתמים לבדיקת מודלים המתבססים על תורתו של פרופ' פנואלי נמצאים בחזית הפיתוח והשימוש התעשייתי בארץ ובעולם.

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

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

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

קורות חיים

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

נשוי לאריאלה (לבית פייניק), ולהם שתי בנות, בן ונכד אחד.

לימודים והשתלמויות

1958–1962 B.Sc. במתמטיקה (בהצטיינות יתרה) בטכניון
1962–1967 דוקטורט (במסלול ישיר) במחלקה למתמטיקה שימושית במכון ויצמן למדע בהנחיית: פרופ' ח"ל פקריס (הנושא: "גיאות ושפל באגנים פשוטים")
1967–1968 פוסט-דוקטורט במחשבים באוניברסיטת סטנפורד ובמרכז המחקר של IBM ב-Yorktown Heights

תפקידים אקדמיים ומחקריים

1969–1973 חוקר בכיר במחלקה למתמטיקה שימושית במכון ויצמן למדע
1973–1980 פרופסור חבר בחוג למדעי המחשב באוניברסיטת תל-אביב (ייסד את החוג ועמד בראשו)
1976–1977 פרופסור אורח אוניברסיטת פנסילבניה
1980– פרופסור מן המניין במחלקה למדעי המחשב ומתמטיקה שימושית במכון ויצמן למדע
1982 פרופסור אורח באוניברסיטת הרווארד
1986 פרופסור אורח באוניברסיטת אוסטין
1977– מחקרים ופיתוחים מקוריים בתחום לוגיקת הזמן (Temporal Logic)
1969– מחקרים ופיתוח כלים בתחום של אפיון תוכנה ואימותה

תפקידים בתעשיית המחשבים

1971 מייסד שותף של חברת "מיני מערכות" לשירותי תוכנה שפעלה במסגרת "סאיטקס" וסיפקה שירותים גם למרכז לטכנולוגיה חינוכית, לתעשייה האווירית ולמערכת ביטחון ונמכרה ל"סאיטקס" ב-1982.
1982 מייסד שותף של חברת "אדקאד" לבניית כלי תכנון ופירוט של מערכות תגובתיות בעזרת שפת ה-Statecharts, שהפכה לחברת I-Logix בשנת 1988.

פרסים ותוארי כבוד

1996 "פרס טורינג" מטעם ACM, הארגון הבין-לאומי למחשבים – הפרס היוקרתי בעולם לאנשי מחשבים
1997 דוקטורט כבוד מטעם אוניברסיטת אופסלה, שבדיה
1998 דוקטורט כבוד מטעם אוניברסיטת יוסף פורייה שבגרנובל, צרפת
1999 חבר זר באקדמיה הלאומית להנדסה, ארה"ב

מפעל חיים

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

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

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

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

אמיר פנואלי נולד בשנת 1941 בנהלל. הוריו, הניה ופרופ' ש"י פנואלי, עלו ארצה ב-1936. תחילה התיישבו בנהלל, ושם ניהל ש"י פנואלי את בית הספר המקומי של המושב. ב-1945 עברה משפחת פנואלי להתגורר בחולון, שכן האב נתמנה למורה בבית המדרש למורים בגבעת השלושה, וברבות הימים נתמנה למנהלו. לאחר מכן היה ש"י פנואלי ממקימי אוניברסיטת תל-אביב ומייסד החוג לספרות עברית שבראשו עמד עד יום מותו, בשנת 1965.

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

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

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

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

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

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

בשנת 1980 חזר אמיר פנואלי למכון ויצמן כפרופסור מלא במחלקה למדעי המחשב ולמתמטיקה שימושית.

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

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

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

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

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

פרסומים נבחרים

  • חיבר 2 ספרים יחד עם פרופ' זהר מנה מאוניברסיטת סטנפורד, לסיכום המתודולוגיה הטמפורלית.

    פרסם מאמרים מדעיים בעיתונות המדעית ברחבי העולם בנושאי מחשב שונים.