Basic HTML Version
™ À ¡ ∂ ¡ ∆ ∂ À • ∏
?
"¶Ú¤ÂÈ Ó· ‰Ôı› ‚¿ÚÔ˜ ÛÙËÓ ÚÔÒıËÛË
Ù˘ Ù¯ÓÔÏÔÁ›·˜ ÛÙËÓ ∂ÏÏ¿‰·"
√ πˆÛ‹Ê ™ËÊ¿Î˘, Ô ŒÏÏËÓ·˜ ÂÚ¢ÓËÙ‹˜ Ô˘ ‚Ú·‚‡ÙËΠ̠ÙË ÛËÌ·ÓÙÈÎfiÙÂÚË ‰ÈÂıÓ‹ ‰È¿-
ÎÚÈÛË ÛÙÔ ¯ÒÚÔ Ù˘ ÏËÚÔÊÔÚÈ΋˜, ÙÔ ‚Ú·‚Â›Ô A.M. Turing, ÌÈÏ¿ÂÈ ÛÙÔ "∫·ÈÓÔÙÔÌ›·, ŒÚ¢ӷ
Î·È ∆¯ÓÔÏÔÁ›·", ÛÙËÓ ∞Ï›ÎË ª·Ú›ÓÔ˘, ÁÈ· ÙÔ ÂÚ¢ÓËÙÈÎfi ÙÔ˘ ¤ÚÁÔ, ·ÏÏ¿ Î·È ÁÈ· ÙȘ ÂÍÂÏ›ÍÂȘ
ÛÙÔÓ ÙÔ̤· ÙÔ˘ ÁÂÓÈÎfiÙÂÚ·: ÁÈ· ÙË ‰È›ۉ˘ÛË Ù˘ Ù¯ÓÔÏÔÁ›·˜ ÛÙËÓ Î·ıËÌÂÚÈÓ‹ ˙ˆ‹, ÙÔ˘˜ ÎÈÓ-
‰‡ÓÔ˘˜ ·ÏÏ¿ Î·È Ù· ÔʤÏË Ô˘ Û˘Ó¿ÁÂÙ·È, ÁÈ· ÙË Û˘Ì‚ÔÏ‹ Ù˘ ÏËÚÔÊÔÚÈ΋˜ ÛÙ· ı¤Ì·Ù·
Ô˘ Ì·˜ ··Û¯ÔÏÔ‡Ó Û‹ÌÂÚ·, fiˆ˜ Ë ÔÈÎÔÏÔÁ›· Î·È Ë ÂÍÔÈÎÔÓfiÌËÛË ÂÓ¤ÚÁÂÈ·˜, Î·È ÁÈ· ÙȘ
ÂÎÏËÎÙÈΤ˜ ÌÂÏÏÔÓÙÈΤ˜ ÂÊ·ÚÌÔÁ¤˜ Ù˘ Ó·ÓÔÙ¯ÓÔÏÔÁ›·˜ Î·È ÙˆÓ ÂÓÛˆÌ·ÙˆÌ¤ÓˆÓ Û˘ÛÙË-
Ì¿ÙˆÓ. ∞ÎfiÌË, Ô π. ™ËÊ¿Î˘ Û¯ÔÏÈ¿˙ÂÈ ÙË ı¤ÛË Ù˘ ¤Ú¢ӷ˜ Î·È Ù˘ Ù¯ÓÔÏÔÁ›·˜ ÛÙËÓ ∂ÏÏ¿‰·
Î·È ÚÔÙ›ÓÂÈ Ì¤ÙÚ· ÁÈ· ÙËÓ Î·Ï‡ÙÂÚË ·ÍÈÔÔ›ËÛË ÙˆÓ ÛËÌ·ÓÙÈÎÒÓ ÏÂÔÓÂÎÙËÌ¿ÙˆÓ Ù˘
¯ÒÚ·˜, fiˆ˜ Â›Ó·È ÙÔ ÂÍ·ÈÚÂÙÈÎfi ·ÓıÚÒÈÓÔ ‰˘Ó·ÌÈÎfi Ù˘.
‹ fi¯È. ∫·È Ì¿ÏÈÛÙ· ÙÔ ÌÔÓÙ¤ÏÔ ÂϤÁ¯ÂÙ·È Î·Ù¿ ÙÚfiÔ ÂÍ·ÓÙÏËÙÈ-
Îfi, ÌÔÚԇ̠ӷ ÂÚÈÙÚ¤ÍÔ˘Ì ‰ËÏ·‰‹ fiϘ ÙȘ ‰˘Ó·Ù¤˜ ηٷ-
ÛÙ¿ÛÂȘ ÙÔ˘ Û˘ÛÙ‹Ì·ÙÔ˜.
√È ‰˘ÛÎÔϛ˜ Ù˘ ÌÂıfi‰Ô˘ Â›Ó·È ‰‡Ô: ÚÒÙÔÓ, Ó· ·Ó·Ù‡ÛÛÔ˘-
Ì ηϿ ÌÔÓ٤Ϸ Î·È ‰Â‡ÙÂÚÔÓ Ó· ÓÈ΋ÛÔ˘Ì ÙËÓ ÔÏ˘ÏÔÎfi-
ÙËÙ· ÙÔ˘ ·ÏÁÔÚ›ıÌÔ˘ ‰ÈÂÚ‡ÓËÛ˘ ÙÔ˘ ÌÔÓÙ¤ÏÔ˘, ηıÒ˜ Ô
·ÚÈıÌfi˜ ÙˆÓ Î·Ù·ÛÙ¿ÛÂˆÓ Ô˘ ÌÔÚ› Ó· ¤¯ÂÈ ¤Ó· ÌÔÓÙ¤ÏÔ
ÌÔÚ› Ó· ÊÙ¿ÛÂÈ ÙȘ ‰È·ÛÙ¿ÛÂȘ ÙÔ˘ ™‡Ì·ÓÙÔ˜.
ªÔÚÔ‡ÌÂ, Û ÔÚÈṲ̂Ó˜ ÂÚÈÙÒÛÂȘ, Ó· ‰ÈÂÚ¢ӋÛÔ˘Ì ÂÍ·-
ÓÙÏËÙÈο ÙȘ ηٷÛÙ¿ÛÂȘ -fi¯È ‚¤‚·È· Ì›·-Ì›·, ÁÈ·Ù› ÙfiÙ ı· ¯ÚÂÈ-
·˙fiÙ·Ó ¿Ú· Ôχ˜ ¯ÚfiÓÔ˜- ·ÏÏ¿ ·›ÚÓÔÓÙ·˜ ·Î¤Ù· ηٷÛÙ¿-
ÛˆÓ. À¿Ú¯Ô˘Ó ‰È¿ÊÔÚ˜ Ù¯ÓÈΤ˜ ÔÈ Ôԛ˜ οÓÔ˘Ó ÙË Ì¤ıÔ-
‰Ô ÂÊ·ÚÌfiÛÈÌË.
¶ÔÈ· ‹Ù·Ó Ë ·ÓÙ·fiÎÚÈÛË ·fi ÙȘ ÂÙ·ÈÚ›˜ ÏËÚÔÊÔÚÈ΋˜;
∆Ô model checking ÂÊ·ÚÌfiÛÙËΠηْ ·Ú¯¿˜ ÛÙÔ hardware.
∞fi Ù· ̤۷ Ù˘ ‰ÂηÂÙ›·˜ ÙÔ˘ ’90 ÂÙ·ÈÚ›˜ fiˆ˜ Ë Intel ‰ËÌÈ-
Ô‡ÚÁËÛ·Ó ÌÂÁ¿Ï· ÂÚÁ·ÛÙ‹ÚÈ· Î·È ·Ó¤Ù˘Í·Ó ÙËÓ Ù¯ÓÔÏÔÁ›·
ÁÈ· Ó· οÓÔ˘Ó Â·Ï‹ı¢ÛË ÛÙ· chips Ù· ÔÔ›· ηٷÛ΢¿-
˙Ô˘Ó. ∞ÚÁfiÙÂÚ· ÂÊ·ÚÌfiÛÙËÎÂ Î·È ÛÙÔ software Î·È Â›Ó·È ÌÈ·
Ù¯ÓÔÏÔÁ›· Ô˘ ¯ÚËÛÈÌÔÔÈÂ›Ù·È Û‹ÌÂÚ· Û ‚ÈÔÌ˯·ÓÈ΋ ÎÏ›-
̷η, ·fi ÂÙ·ÈÚ›˜ fiˆ˜ Ë Microsoft Î·È Ë IBM.
¶ÈÛÙ‡ÂÙ fiÙÈ ÙÔ Model Checking ¤¯ÂÈ ‰˘Ó·ÙfiÙËÙ· Ó· ÂÊ·ÚÌÔ-
ÛÙ› Û οı ηٷÛ΢‹ ÏËÚÔÊÔÚÈ·ÎÔ‡ Û˘ÛÙ‹Ì·ÙÔ˜ ‹ ˘¿Ú-
¯Ô˘Ó fiÚÈ· ÛÙËÓ ÂÊ·ÚÌÔÁ‹ ÙÔ˘;
À¿Ú¯Ô˘Ó ÔÚÈṲ̂ӷ fiÚÈ·. ªÔÚ› Ó· ÂÊ·ÚÌÔÛÙ› Û¯ÂÙÈο ‡ÎÔ-
Ï· Û hardware, ·ÏÏ¿ ÏÈÁfiÙÂÚÔ Â‡ÎÔÏ· Û software. ∞˘Ùfi ÔÊ›-
ÏÂÙ·È ÛÙË ‰˘ÛÎÔÏ›· ·Ú·ÁˆÁ‹˜ Ì·ıËÌ·ÙÈÎÒÓ ÌÔÓÙ¤ÏˆÓ ÁÈ· ÙÔ
software, ÂȉÈο ·˘Ùfi Ô˘ ¯ÚËÛÈÌÔÔÈÂ›Ù·È ÛÙÔ˘˜ ÔÈÎÈ·ÎÔ‡˜ ∏/À.
∞ÓÙ›ıÂÙ·, ÙÔ software Ô˘ ¯ÚËÛÈÌÔÔÈÂ›Ù·È ÛÙ· ·ÂÚÔÏ¿Ó·, ¤Ó·˜
ÙÔ̤·˜ ÛÙÔÓ ÔÔ›Ô ¤¯ˆ ÂÚÁ·ÛÙ›, Â›Ó·È Ôχ ÈÔ ·Ïfi. ™ÙÔȯ›˙ÂÈ
ÂÚÈÛÛfiÙÂÚÔ ÛÙȘ ÂÙ·ÈÚ›˜ Ó· ÊÙÈ¿ÍÔ˘Ó ·Ïfi software, ·ÏÏ¿ ÙÔ
οÓÔ˘Ó ÁÈ· Ó· ÌÔÚ› Ó· Â›Ó·È Â·ÏËı‡ÛÈÌÔ.
∆È ÛËÌ·›ÓÂÈ ÁÈ· Û·˜ Î·È ÁÈ· ÙÔ ÂÚ¢ÓËÙÈÎfi Û·˜ ¤ÚÁÔ Ë ‚Ú¿‚¢-
Û‹ Û·˜ Ì ÙÔ ‚Ú·‚Â›Ô Turing;
∂›Ó·È ÌÈ· ‰ÈÂıÓ‹˜ ·Ó·ÁÓÒÚÈÛË, Ë ÌÂÁ·Ï‡ÙÂÚË ÛÙÔÓ ÙÔ̤· ÌÔ˘,
Î·È ÁÈ’ ·˘Ùfi ‚¤‚·È· Â›Ó·È Î¿ÙÈ ÛËÌ·ÓÙÈÎfi ÁÈ· ̤ӷ. ∏ ·Ó·ÁÓÒÚÈ-
ÛË ·˘Ù‹ ¤Ú¯ÂÙ·È ÌÂÙ¿ ÔÏÏ¿ ¯ÚfiÓÈ·, ÁÈ·Ù› Ì ÙÔ ‚Ú·‚Â›Ô ·˘Ùfi
·Ó·ÁÓˆÚ›˙ÂÙ·È ÙÔ ¤ÚÁÔ Ô˘ Ú·ÁÌ·ÙÔÔ›ËÛ· ηٿ ÙË ‰ÂηÂÙ›·
ÙÔ˘ 1980. ∞Û¯ÔÏ‹ıËη Ì ÙÔÓ ÙÔ̤· ÙÔ˘ model checking
Á‡Úˆ ÛÙ· 15-20 ¯ÚfiÓÈ·. ∏ ÚÒÙË Û¯ÂÙÈ΋ ‰ËÌÔÛ›Â˘ÛË ·Ó·ÎÔÈ-
ÓÒıËΠÙÔ 1982, ·Ó Î·È Ù· ·ÔÙÂϤÛÌ·Ù· ›¯·Ó ‚ÁÂÈ 3-4 ¯Úfi-
ÓÈ· ÓˆÚ›ÙÂÚ·. ¢Ô‡Ï¢· ·Ú¿ÏÏËÏ· Ì ÙÔ˘˜ ¿ÏÏÔ˘˜ ‰‡Ô Û˘Ó·-
‰¤ÏÊÔ˘˜ Ì ÙÔ˘˜ ÔÔ›Ô˘˜ ÌÔÈÚ·ÛًηÌ ÙÒÚ· ÙÔ ‚Ú·‚›Ô
Turing. ¶·ÚfiÏÔ Ô˘ ‰ÂÓ Û˘ÓÂÚÁ·ÛًηÌ ÂÚ¢ÓËÙÈο, ÎÈÓËÙÔ-
ÔÈ‹Û·Ì ̷˙› ÙÔ˘˜ Û˘Ó·‰¤ÏÊÔ˘˜ ÒÛÙ ӷ ‰ËÌÈÔ˘ÚÁ‹ÛÔ˘ÌÂ
ÌÈ· ÎÔÈÓfiÙËÙ· ÁÈ· ÙÔ model checking.
¶ÔȘ Â›Ó·È ÔÈ ‚·ÛÈΤ˜ ·Ú¯¤˜ ÙÔ˘ ªodel Checking;
H ÏËÚÔÊÔÚÈ΋ Â›Ó·È ÌÈ· ÂÈÛÙ‹ÌË 60 ÌfiÓÔ ÂÙÒÓ Î·È ‚Ú›ÛÎÂÙ·È
·ÎfiÌ· ÛÙÔÓ ªÂÛ·›ˆÓ· Ù˘ ÂͤÏÈÍ‹˜ Ù˘. ¢ÂÓ ˘¿Ú¯ÂÈ Ì¤ıÔ‰Ô˜
ÁÈ· ÙÔ Û¯Â‰È·ÛÌfi ÙˆÓ Û˘ÛÙËÌ¿ÙˆÓ, Ù· ÔÔ›· ۯ‰ȿ˙ÔÓÙ·È ÂÌÂÈ-
ÚÈο ÂÓ ÔÏÏÔ›˜. ª¿ÏÈÛÙ·, fiÙ·Ó Î¿ÓÔ˘Ì ÌÂÁ¿Ï· Û˘ÛÙ‹Ì·Ù·, Ù·
Ú›Ûη Ô˘ ·›ÚÓÔ˘ÌÂ Â›Ó·È ÌÂÁ¿Ï·. ™‡Ìʈӷ Ì ÙȘ ÛÙ·ÙÈÛÙÈΤ˜,
Û οı 100 ¤ÚÁ· ÁÈ· ÌÂÁ¿Ï· Û˘ÛÙ‹Ì·Ù·, 40 ·ÔÙ˘Á¯¿ÓÔ˘Ó, 30
¤¯Ô˘Ó ̤ÙÚÈ· ÂÈÙ˘¯›· Î·È ÌfiÓÔ 30 ıˆÚÔ‡ÓÙ·È ÂÈÙ˘¯Ë̤ӷ.
∏ ȉ¤· ›Ûˆ ·fi ÙË ‰Ô˘ÏÂÈ¿ Ô˘ οӷÌ Ì ÙÔ˘˜ Û˘Ó·‰¤ÏÊÔ˘˜
Â›Ó·È fiÙÈ ·ÓÙ› Ó· ·Ó·Ù‡ÛÛÔ˘Ì ¤Ó· Û‡ÛÙËÌ· Î·È Ó· ÚÔÛ·-
ıԇ̠̤۷ ·fi ¤ÏÂÁ¯Ô Ó· ÂȂ‚·ÈÒÛÔ˘Ì fiÙÈ ÏÂÈÙÔ˘ÚÁ›
ÛˆÛÙ¿, Ó· ‰ËÌÈÔ˘ÚÁԇ̠¤Ó· ÂÈÎÔÓÈÎfi ÚˆÙfiÙ˘Ô (virtual
prototype), ÙÔ ÔÔ›Ô Ï¤Ì ÌÔÓÙ¤ÏÔ, Î·È ÙÔ ÔÔ›Ô ÌÔÚԇ̠ӷ
ÂϤÁÍÔ˘ÌÂ. ∏ ̤ıÔ‰Ô˜ ÏÔÈfiÓ ÙÔ˘ model checking Û˘Ó›ÛٷٷÈ
ÛÙÔÓ ¤ÏÂÁ¯Ô ÂÓfi˜ ÌÔÓÙ¤ÏÔ˘ ÙÔ ÔÔ›Ô ·Ó··ÚÈÛÙ¿ ÙË ÏÂÈÙÔ˘ÚÁ›·
ÙÔ˘ Û˘ÛÙ‹Ì·ÙÔ˜, Ì ÔÚÈṲ̂Ó˜ ÏÂÈÙÔ˘ÚÁÈΤ˜ ··ÈÙ‹ÛÂȘ Ô˘
¤¯Ô˘Ì ·fi ·˘Ùfi. ∏ ¤Ú¢ӷ ·ÊÔÚÔ‡Û ÙËÓ ·Ó¿Ù˘ÍË ·ÏÁÔÚ›ı-
ÌˆÓ Ô˘ Û˘ÁÎÚ›ÓÔ˘Ó ÙÔ ÌÔÓÙ¤ÏÔ Ì ÙȘ ÏÂÈÙÔ˘ÚÁÈΤ˜ ··ÈÙ‹-
ÛÂȘ Î·È ·ÔÊ·Û›˙Ô˘Ó Â¿Ó ÔÈ ··ÈÙ‹ÛÂȘ ·˘Ù¤˜ ÈηÓÔÔÈÔ‡ÓÙ·È
™˘Ó¤ÓÙ¢ÍË Ì ÙÔÓ πˆÛ‹Ê ™ËÊ¿ÎË,
¢È¢ı˘ÓÙ‹˜ ∂Ú¢ÓÒÓ ÛÙÔ CNRS, ‚Ú·‚Â›Ô ∞.ª. ∆uring 2007
∫∞ π¡√∆√ªπ ∞
∂ƒ∂À¡∞ ∫∞π ∆∂á√§√°π∞
2 4