מאגר מידע בנושאי מחשבים ומדעים מדויקים
שפות תיכנות
שפת C#
שפת C
שפת C++
Java
אסמבלר
SQL
שפות פונקציונליות
Python
Perl
DirectX
Visual Basic
פסקל
mIRC Scripts
שונות
בניית אתרים
HTML
DHTML
ASP
ASP.Net
PHP
קידום אתרים
שונות
אבטחת מידע ו-IT
Web Security
אנונימיות, פרטיות וחוק ברשת האינטרנט
קריפטוגרפיה
הנדסה לאחור (reversing)
אבטחת ססמאות
אבטחת מידע - כללי
טרוינים ווירוסים
אבטחת Windows
מגזין IKP
מערכות ההפעלה Unix/Linux
מערכת ההפעלה DOS
מערכות הפעלה - כללי
מערכת ההפעלה XINU
חומרה
רשתות
פרוטוקולים - השכבה הפיסית
פרוטוקולים - שכבת האפליקציה
עולם ה-Web
צ'טים
מדריכי תוכנות
משחקים
מיקרואלקטרוניקה
מגזין Digital Whisper
:
Digital Whisper - גליונות מלאים
Digital Whisper - הגליון הראשון
Digital Whisper - הגליון השני
Digital Whisper - הגליון השלישי
Digital Whisper - הגליון הרביעי
Digital Whisper - הגליון החמישי
Digital Whisper - הגליון השישי
Digital Whisper - הגליון השביעי
Digital Whisper - הגליון השמיני
Digital Whisper - הגליון התשיעי
Digital Whisper - הגליון העשירי
Digital Whisper - הגיליון האחד עשר
Digital Whisper - הגיליון השנים עשר
Digital Whisper - הגיליון השלושה עשר
Digital Whisper - הגיליון הארבעה עשר
Digital Whisper - הגיליון החמישה עשר
Digital Whisper - הגיליון השישה עשר
Digital Whisper - הגיליון השבעה עשר
Digital Whisper - הגיליון השמונה עשר
Digital Whisper - הגיליון התשעה עשר
Digital Whisper - הגיליון העשרים
Digital Whisper - הגיליון העשרים ואחד
Digital Whisper - הגיליון העשרים ושניים
Digital Whisper - הגיליון העשרים ושלושה
Digital Whisper - הגיליון העשרים וארבעה
Digital Whisper - הגיליון העשרים וחמישה
Digital Whisper - הגיליון העשרים ושישה
Digital Whisper - הגיליון העשרים ושבעה
Digital Whisper - הגיליון העשרים ושמונה
Digital Whisper - הגיליון העשרים ותשעה
Digital Whisper - הגיליון השלושים
Digital Whisper - הגיליון השלושים ואחד
Digital Whisper - הגיליון השלושים ושניים
Digital Whisper - הגיליון השלושים ושלושה
Digital Whisper - הגיליון השלושים וארבעה
מדעי המחשב
אלגוריתמים בתורת הגרפים
מבני נתונים
ביטויים רגולריים
לוגיקה
הנדסת תוכנה
אוטומטים ושפות פורמליות
שפות תכנות
בינה מלאכותית
מערכות לומדות
תכנות מונחה אספקטים
ניהול זיכרון דינמי
Design Patterns
תכנות מונחה עצמים
תורת החישוביות
עיבוד אותות
מתמטיקה
אלגברה מודרנית
אלגברה לינארית
מתמטיקה דיסקרטית
חשבון דיפרנציאלי ואינטגרלי
מבוא להסתברות והתפלגויות
משוואות דיפרנציאליות רגילות
משוואות דיפרנציאליות חלקיות
מתמטיקה תיכונית
אנליזה נומרית
טורי פורייה
תורת המשחקים
פונקציות מרוכבות
שונות
סטטיסטיקה
טופולוגיה
גיאומטריה
כלכלה
חקר ביצועים
פיסיקה
אלקטרוניקת הספק
פיסיקה תיכונית
פיסיקה 1
פיסיקה 2
פיסיקה קוונטית
מכניקה אנליטית
אלקטרומגנטיקה
פיסיקה 3
שונות
עמוד הבית
>
מדעי המחשב
>
הנדסת תוכנה
>
מבוא לאימות תוכנה
>
לוגיקות טמפורליות
הועלה לאתר:
מספר עמודים: 120
להורדת המסמך בשלמותו
מבוא לאימות תוכנה
ספר אלקטרוני
מאת:
ניר אדר
7.4. לוגיקות טמפורליות
נושאים בפרק זה:
CTL*
CTL
LTL
הגדרת האופרטורים הטמפורלים – ויקיפדיה האנגלית
תגיות המסמך:
הנדסת תוכנה
אימות תוכנה
ישויות מתמטיות
אמות
מודלים
מבוא
לוגיקה
הנדסה
בדיקה
תכנה
לפרק הקודם
7.3. מערכת ההוכחה
H*
לפרק הבא
7.4.1.
CTL*
אין תגובות!
דיווח על הפרת זכויות יוצרים
תוכן העניינים:
מבוא
לוגיקה מסדר ראשון - תקציר
תזכורת – תחשיב היחסים
תזכורת – מונחים מעולם הלוגיקה
הוכחת נכונות של תוכניות
הגדרות בסיסיות
חישוב של תוכנית
תכונה של תוכנית - נכונות חלקית
הגדרה
דוגמא למצב בעייתי
תכונה של תוכנית - נכונות מלאה
תרשימי זרימה – Flowcharts
הגדרות
סמנטיקה
למת ההפרדה
שיטת / כללי ההוכחה
הגדרות – טרנספורמצית המצבים, תנאי הישיגות
דוגמאות לעבירות
הגדרה אינדוקטיבית של
ושל
כלל להוכחת נכונות עבור תוכניות ללא מעגלים
כלל ההוכחה F
(
(Floyd
לתוכניות תרשים זרימה עם חוגים
יתרונות וחסרונות שיטת Floyd
דוגמא להפעלת Floyd
נאותות ושלמות שיטת Floyd
הוכחת עצירה של תוכניות בשפת PLF
קבוצה מבוססת היטב
כלל
F*
להוכחת עצירה
לוגיקה של תוכניות
הגישה המודולרית של Hoare
שפת תוכניות while
רלציית המעברים
למת החישובים
מערכת הוכחה H
להוכחת נכונות חלקית
אקסיומות
כללי הסק
משפט הנאותות של H
משפט השלמות של H
קצת פרקטיקה
מערכת
H*
להוכחת
אימות אוטומטי - שיטות לבדיקת מודל
מבוא
מבנה קריפקה - Kripke Structure
לוגיקות טמפורליות פסוקיות
מרכיבי הלוגיקות הטמפורליות
אופרטורים טמפורליים
CTL*
הגדרת
CTL*
הגדרה אינדוקטיבית של
דוגמאות לנוסחאות + משמעות אינטואיטיבית
CTL
LTL
זיהוי ביטויים מהלוגיקות השונות
אלגוריתם מפורש לבדיקת מודל CTL
הבעיה והאלגוריתם
תרגילים
סיבוכיות בדיקת מודל
הוספת הוגנות ל-CTL
הגדרות ודוגמאות ראשונות
סמנטיקה
אלגוריתם לחישוב קבוצת המצבים המספקים
טיפול ב-
דוגמא
BDD
- Binary Decision Diagram
תיאור קבוצה ע"י פונקציה בוליאנית
יצוג מבנה קריפקה על ידי פונקציה בוליאנית - דוגמא
BDD
- דוגמא ראשונה
BDD
כמבנה נתונים
פעולות על BDDs
:
פעולת צמצום –
(Reduce)
פעולת הגבלה - restriction
פעולות בוליאניות על BDD
(Apply
)
פעולת not
יצוג מבנה קריפקה בעזרת BDD
בדיקת מודל סימבולית מבוססת BDD
מבוא והגדרות
פעולות על קבוצות
בדיקת מודל סימבולית לפי מבנה הנוסחה
דוגמאות
Reachable
תיאור אלמנטים בגרף באמצעות BDD
בדיקת מודל סימבולית מבוססת SAT
תזכורת – בעיית SAT
בדיקת מודל מבוססת SAT
– Bounded Model Checking
הוכחת נכונות בעזרת SAT
– Unbounded Model Checking
תרגילים ודוגמאות
תרגיל 1
פתרונות לבעיית SAT
– SAT Solver
מבוא והצגה חוזרת של הבעיה
אלגוריתם בסיסי לפתרון SAT
-
Davis Putmam
(DPLL
), 1960, 1962
שיפור לאלגוריתם – יוריסטיקה לבחירת המשתנה הבא שיקבל ערך
שיפור לאלגוריתם – שימוש במבנה נתונים חכם לזרוז BCP
שיפור לאלגוריתם - למידה
נוסחאון
למת החישובים
מערכת ההוכחה H
מערכת ההוכחה
H*
לוגיקות טמפורליות
CTL*
CTL
LTL
הגדרת האופרטורים הטמפורלים – ויקיפדיה האנגלית
חשוב לזכור
מקורות
מקורות בעברית
מקורות באנגלית
קישורים רלוונטיים:
מדעי המחשב
שיתוף:
|
עוד