מערכת זמן אמת – הבדלי גרסאות

מתוך ויקיפדיה, האנציקלופדיה החופשית
תוכן שנמחק תוכן שנוסף
Alonr (שיחה | תרומות)
מאין תקציר עריכה
Yonidebot (שיחה | תרומות)
מ בוט החלפות: לעתים;
שורה 14: שורה 14:


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



גרסה מ־14:55, 11 ביולי 2009

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

סוגי מערכות

מערכות זמן אמת נחלקות לשני סוגים:

Hard real-time

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

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

בשל האיטיות היחסית של אחסון הזיכרון המשני, במערכות Hard real-time, שטח הזיכרון המשני מוגבל או שלא נעשה בו כלל שימוש והמידע מאוחסן בזיכרון קצר טווח או בזיכרון לקריאה בלבד (ROM). קיים קונפליקט בין דרישות אלו לדרישות של time-sharing systems, ולכן שילוב כזה לא נתמך על ידי מערכות הפעלה שנועדו למגוון מטרות (להבדיל ממערכות הפעלה ייעודיות).

Soft real-time

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

פיתוח מערכות זמן אמת בגישה פורמלית

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

ראו גם