VeriTech: פרויקט לתרגום ושילוב בין מפרטים וכלי אימות

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

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

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

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

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

קיום הגרעין מאפשר להוסיף יכולות אימות חדשות לכלים השונים המשולבים ב- VeriTech על-ידי הוספת יכולות אלו כטרנספורמציות למצגת הגרעין. כדוגמא, ניתן להוסיף לגרעין שיטות לצמצום מרחב המצבים שמסתמכות על הפשטה (abstraction) וסדר חלקי(partial order) .

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

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

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

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

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

כשלב ראשון בפתוח VeriTech הבאנו גרסאות קיימות של מגוון כלי אמות זמינים לציבור. הכלים מכסים ספקטרום רחב של שיטות. רשימה חלקית כוללת: PVS - כלי להוכחת משפטים בלוגיקה. SteP - כלי לאימות תכניות ביחס למפרטים בלוגיקה טמפורלית מסדר ראשון. SMV ו- SPIN – כלים שמסתמכים על אלגוריתמים לבדיקת מודל (model checking algorithms) ומאפשרים אימות אוטומטי של מערכות בעלות מספר מצבים סופי ביחס למפרטים בלוגיקה טמפורלית פסוקית. SMV מתאים במיוחד לאימות מעגלים חשמליים, ואילו SPIN מתאים לאימות פרוטוקולי תקשורת. LOTOS ו- Concurrency Workbench - מתבססים על השוואת המפרט והמערכת, כששניהם כתובים באותה שפה. Murphi – מוודא נכונות המערכת על-ידי חישוב כל המצבים הישיגים של המערכת ובדיקה שכל אחד מהם עומד במפרט.

כאשר המערכות המתוארות לעיל הותקנו, הפעלנו אותם על דוגמאות טיפוסיות (case studies), שבמסגרתן בדקנו את הדומה והשונה בייצוג של מערכת ומפרט נתונים בכלים השונים. ההשוואה נעשתה עבור תיכון מעגל חומרה (אסינכרוני וסינכרוני – תוך שימוש ב- LOTOS, SMV) ותוכנה (תוך שימוש ב- PVS, Murphi). בין הדוגמאות יש גרסאות של arbiters , יישום של מבני נתונים פשוטים stacks and queues)) ואלגוריתמים למניעה הדדית (mutual exclusion).

אבות טיפוס של תרגומים יושמו משפות תיכון שונות אל מצגת הגרעין. בשלב ראשון, נבחרה מערכת מעברים פשוטה כשפה לתיאור המערכת בגרעין. מטרת תרגומים אלה הייתה לזהות אספקטים בעייתיים ומושגים מודולריים (modularity concepts) שהם קשים לתפיסה, כתמריץ לתכנון שפת גרעין יותר מובנית. אבות הטיפוס נבנו עבור Murphi, SMV ו- CCS (דרך Concurrency Workbench). למרות שיושם רק התרגום מהשפה של כלי האימות אל מערכת המעבר של הגרעין, הבעיות בתרגום בכיוון הנגדי נותחו גם הן.

זוהו בעיות מפתח בתרגום, שהן מעבר לאנליזה סינטקטית רגילה ופעולות אינדיבידואליות המיוחדות לכל שפה. ראשית, השפות נבדלות משמעותית בהגדרת הפעולות האטומיות שלהן grain of atomicity) ). ב- Murphi למשל, החוקים למעבר בין מצבי מערכת יכולים להכיל קוד C כלשהו ועם זאת להיחשב אטומיים. בתרגום אל מערכת המעברים של הגרעין אי אפשר לתרגם חוק כזה למעבר יחיד, שבו השינוי מבוטא ביחס יחיד. זה נכון במיוחד כאשר יש לולאות בתוך הקוד של החוק.

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

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

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

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

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

ישנן תכניות להמשך שתוף הפעולה עם תעשיית התכנה והחמרה הן בנושאי מימון והן בהפעלת VeriTech על דוגמאות מציאותיות.

לפרטים נוספים, בקרו באתר האינטרנט של VeriTech: http://www.cs.technion.ac.il/users/veritech