X-apparati - X-machine

The X-apparati (XM) ning nazariy modeli hisoblanadi hisoblash tomonidan kiritilgan Samuel Eilenberg 1974 yilda.[1]The X "X-machine" da mashina ishlaydigan asosiy ma'lumotlar turini aks ettiradi; masalan, ma'lumotlar bazalarida ishlaydigan mashina (turdagi ob'ektlar ma'lumotlar bazasi) bo'lardi ma'lumotlar bazasi- mashina. X-mashina modeli strukturaviy jihatdan xuddi shunday cheklangan davlat mashinasi, bundan tashqari, mashinaning o'tishini belgilash uchun ishlatiladigan belgilar munosabatlar turdagi X→X. O'tishni kesib o'tish, uni belgilaydigan munosabatni qo'llashga teng (ma'lumotlar turiga o'zgartirishlar to'plamini hisoblash) X) va mashinadagi yo'lni bosib o'tish barcha bog'liq munosabatlarni ketma-ket qo'llashga mos keladi.

Asl nazariya

Eilenbergning asl X-apparati hisoblashning umuman umumiy nazariy modeli edi Turing mashinasi masalan, deterministik, deterministik bo'lmagan va tugamaydigan hisob-kitoblarni tan olgan. Uning asosiy ishi [1] asosiy X-mashinalar modelining ko'plab variantlarini nashr etdi, ularning har biri cheklangan davlat mashinasi biroz boshqacha tarzda.

Eng umumiy modelda X-mashina mohiyatan "X tipidagi ob'ektlarni boshqarish mashinasi" dir. $ X $ biroz bo'lsa-da, deylik ma'lumotlar turi, deb nomlangan asosiy ma'lumotlar turi, va bu Φ (qisman) munosabatlarning to'plami φ: X → X. X-mashina - bu cheklangan davlat mashinasi o'qlari Φ dagi munosabatlar bilan belgilanadi. Har qanday holatda, bir yoki bir nechta o'tish mumkin yoqilgan agar domen bog'liq munosabatlarning ofmen X da saqlangan joriy qiymatlarni qabul qiladi (bir qism) Har bir tsikldagi barcha yoqilgan o'tish jarayoni qabul qilingan deb hisoblanadi. Mashinadan o'tgan har bir taniqli yo'l a ro'yxatini hosil qiladi1 ... φn munosabatlar. Biz kompozitsiyani call deb ataymiz1 o ... o φn ushbu munosabatlarning yo'l munosabati ushbu yo'lga mos keladi. The xulq-atvor X-mashinasining yo'li munosabatlari bilan hisoblab chiqilgan barcha xatti-harakatlarning birlashishi deb ta'riflanadi. Umuman olganda, bu deterministik emas, chunki har qanday munosabatni qo'llash X bo'yicha natijalar to'plamini hisoblab chiqadi, Rasmiy modelda barcha mumkin bo'lgan natijalar parallel ravishda birgalikda ko'rib chiqiladi.

Amaliy maqsadlar uchun X-apparati ba'zi cheklangan hisoblashni tavsiflashi kerak. A: Y → X kodlash funktsiyasi ba'zilaridan o'zgartiriladi kiritish ma'lumotlar turi Y ning boshlang'ich holatiga X va dekodlash funktsiyasi β: X → Z, X ning oxirgi holatidan (holatlarini) ba'zi holatga qaytaradi chiqish ma'lumotlar turi Z. X ning boshlang'ich holatini to'ldirgandan so'ng, X-mashina oxirigacha ishlaydi va natijada natijalar kuzatiladi. Umuman olganda, mashina blokirovka qilinishi mumkin (bloklanishi mumkin) yoki to'g'ridan-to'g'ri blokirovkasi (hech qachon to'xtamaydi) yoki bir yoki bir nechta to'liq hisoblashni amalga oshirishi mumkin. Shu sababli, so'nggi tadqiqotlar xulq-atvorini aniqroq kuzatish va kuzatish mumkin bo'lgan deterministik X-mashinalarga qaratilgan.

Misol

Peep-hole optimizatoriga ega bo'lgan kompilyatorni dastur tuzilishini optimallashtirish uchun mashina deb hisoblash mumkin. Bunda Optimizator- mashina, a kodlash funktsiyasi kirish kodi Y (dastur manbai) dan manba kodini oladi va uni X (xotira turi) xotirasiga yuklaydi. Mashinaning bir nechta holati bor deylik FindIncrements, FindSubExprs va Bajarildi. Mashina dastlabki holatida boshlanadi FindIncrementso'tish davri orqali boshqa davlatlar bilan bog'langan:

 FindIncrements →DoIncrement FindIncrements FindIncrements →O'tkazib yuborish FindSubExprs FindSubExprs →DoSubExpr FindSubExprs FindSubExprs →SkipSubExpr Bajarildi

Aloqalar DoIncrement "x: = x + 1" ga mos keladigan ajratilgan kichik daraxtni optimallashtirilgan "++ x" kichik daraxtga qo'shadi. Aloqalar DoSubExpr "z: = x + y; ... z ..." hisob-kitobini saqlash uchun lokal o'zgaruvchiga ega bo'lgan optimallashtirilgan versiyada bir xil "x + y ... x + y" ifodasini o'z ichiga olgan tahlil daraxtini xaritalaydi. z ". Ushbu aloqalar faqat Xda ular ishlaydigan domen qiymatlarini (subtrees) o'z ichiga olgan taqdirda yoqiladi. Qolgan munosabatlar O'tkazib yuborish va SkipSubExpr bor nulloplar (identifikatsiya munosabatlari) qo'shimcha holatlarda faollashtirilgan.

Shunday qilib, Optimizator-machine oxirigacha ishlaydi, avval ahamiyatsiz qo'shimchalarni joyiga oshirishga aylantiradi (da esa FindIncrements davlat), keyin u ga o'tadi FindSubExprs holatini aniqlang va bir qator umumiy sub-ifodalarni olib tashlashni amalga oshiring, shundan so'ng u oxirgi holatga o'tadi Bajarildi. Shunda dekodlash funktsiyasi X xotira turidan (optimallashtirilgan tahlil daraxti) Z tipiga (optimallashtirilgan mashina kodi) to'g'ri keladi.

Konventsiya

Eilenbergning asl modeli haqida gap ketganda, "X-mashina" odatda kichik harf "m" bilan yoziladi, chunki bu ma'no "Xni qayta ishlash uchun har qanday mashina" dir. Keyinchalik o'ziga xos modellarga murojaat qilganda, konventsiya ushbu variantning tegishli nomining bir qismi sifatida "M" harfidan foydalanishni anglatadi.

1980-yillar

X-apparatga qiziqish 1980-yillarning oxirida Mayk Xolkom tomonidan qayta tiklandi,[2] model dasturiy ta'minot uchun juda mos ekanligini payqagan rasmiy spetsifikatsiya maqsadlar, chunki u toza ajralib chiqadi oqim oqimi dan qayta ishlash. Agar etarli darajada mavhum darajada ishlash sharti bilan, hisoblashdagi boshqaruv oqimlari odatda cheklangan holatdagi mashina sifatida ifodalanishi mumkin, shuning uchun X-mashinaning spetsifikatsiyasini bajarish uchun mashinaning har bir o'tishi bilan bog'liq ishlov berishni belgilash qoladi. Modelning strukturaviy soddaligi uni nihoyatda moslashuvchan qiladi; g'oyaning boshqa illyustratsiyalarida Xolkomning inson-kompyuter interfeyslari xususiyati,[3]hujayra biokimyosidagi jarayonlarni modellashtirish,[4]va Stannettning harbiy qo'mondonlik tizimlarida qaror qabul qilishni modellashtirish.[5]

1990-yillar

X-mashinalari 1990-yillarning o'rtalaridan boshlab, Gilbert Laycockning deterministik davridan boshlab yangi e'tiborga sazovor bo'ldi Stream X-Machine[6] katta dasturiy ta'minot tizimlarini aniqlash uchun asos bo'lib xizmat qilganligi aniqlandi to'liq sinovdan o'tkazilishi mumkin.[7] Boshqa variant, Stream X-Machine-ni aloqa qilish biologik jarayonlar uchun foydali sinovdan o'tkaziladigan modelni taklif etadi[8] va kelajak to'daga asoslangan sun'iy yo'ldosh tizimlari.[9]

2000-yillar

X-apparatlar qo'llanildi leksik semantika tomonidan Andras Kornai So'z ma'nosini X tayanch to'plamining bitta a'zosi ajratilgan "uchli" mashinalar yordamida modellashtiradi.[10] Tilshunoslikning boshqa sohalariga, xususan, zamonaviy islohotlarga murojaat qilish Pokini tomonidan kashshof bo'lgan Jerar Xuet va uning hamkasblari[11][12]

Asosiy variantlar

X-apparati kamdan-kam hollarda asl shaklida uchraydi, ammo hisoblashning bir nechta keyingi modellari asosida ishlaydi. Dasturiy ta'minotni sinash nazariyalaridagi eng ta'sirchan model bu bo'ldi Stream X-Machine. NASA yaqinda ning kombinatsiyasidan foydalanishni muhokama qildi Oqim rentgen apparatlari bilan aloqa o'rnatish va loyihalashtirishda va sinovdan o'tkazishda WSCSS jarayonini hisoblash to'da sun'iy yo'ldosh tizimlar.[9]

Analog X mashinasi (AXM)

Dastlabki variant, doimiy vaqt Analog X-Machine (AXM), 1990 yilda Mayk Stannett tomonidan potentsial "super-Tyuring" hisoblash modeli sifatida kiritilgan;[13]natijada u ish bilan bog'liq giper hisoblash nazariya.[14]

Stream X-Machine (SXM)

Asosiy maqola: Stream X-Machine

X-machine-ning eng ko'p uchraydigan varianti Gilbert Laycockning 1993 y Stream X-Machine (SXM ) model,[6]bu Mayk Xolkomb va Florentin Ipatning nazariyasi uchun asos bo'lib xizmat qiladi to'liq sinov tugagandan so'ng, ma'lum bo'lgan aniqlik xususiyatlarini kafolatlaydigan dasturiy ta'minotni sinovdan o'tkazish.[7][15] Stream X-Machine Eilenbergning asl modelidan farq qiladi, chunki X ning asosiy ma'lumotlar turi shaklga ega Chiqdi* × Mem × Yilda*, qaerda Yilda* kirish ketma-ketligi, Chiqdi* - bu chiqish ketma-ketligi va Mem bu (qolgan) xotira.

Ushbu modelning afzalligi shundaki, u tizimni har qadamda natijalarni kuzatishda, uning holatlari va o'tishlari orqali birma-bir yurishga imkon beradi. Bu guvohlik qadriyatlari, bu har bir qadamda aniq funktsiyalar bajarilishini kafolatlaydi. Natijada, murakkab dasturiy ta'minot tizimlari yuqoridan pastga qarab ishlab chiqilgan va pastdan yuqoriga qarab sinovdan o'tgan Stream X-Machines ierarxiyasiga aylanishi mumkin. Loyihalash va sinovga bo'linish va zabt etishning bunday yondashuvi Florentin Ipatning to'g'ri integratsiyani isbotlashi bilan tasdiqlangan,[16] bu qatlamli mashinalarni mustaqil ravishda sinovdan o'tkazish tuzilgan tizimni sinab ko'rishga teng bo'lganligini isbotlaydi.

X-Machine (CXM) bilan aloqa o'rnatish

"CXM" qayta yo'naltirishlar. Shu bilan Angola aeroporti uchun IATA kod, qarang Kamaxilo aeroporti.

Bir nechta X-apparatlarni parallel ravishda ulash bo'yicha eng dastlabki taklif Judit Barnardning 1995 yildagi taklifidir X-apparati bilan aloqa o'rnatish (CXM yoki COMX) model,[17][18]unda mashinalar nomlangan aloqa kanallari orqali ulanadi (ma'lum: portlar); ushbu model diskret va real vaqtda variantlarda mavjud.[19] Ushbu asarning oldingi versiyalari to'liq rasmiy bo'lmagan va to'liq kirish / chiqish munosabatlarini ko'rsatmagan.

Buferli kanallardan foydalangan holda o'xshash X-Machine Communication yondashuvi Petros Kefalas tomonidan ishlab chiqilgan.[20][21] Ushbu ishning asosiy yo'nalishi tarkibiy qismlarning ekspresivligiga qaratildi. Kanallarni qayta tayinlash imkoniyati Stream X-Machines-ning ba'zi sinov teoremalari bajarilmasligini anglatardi.

Ushbu variantlar muhokama qilinadi batafsilroq alohida sahifada.

Aloqa oqimi X-Machine (CSXM)

Bir vaqtning o'zida X-machine kompozitsiyasining to'liq rasmiy modeli 1999 yilda Kristina Vertan va Xoriya Georgesku tomonidan taklif qilingan,[22] Filipp Bird va Entoni Kovling tomonidan avtomatlarni aloqa qilish bo'yicha ilgari olib borilgan ishlar asosida.[23] Vertan modelida mashinalar bilvosita, umumiy foydalanib aloqa qilishadi aloqa matritsasi to'g'ridan-to'g'ri umumiy kanallar orqali emas (asosan kaptar teshiklari qatori).

Blesnesku, Kovling, Georgesku, Vertan va boshqalar ushbu CSXM modelining rasmiy xususiyatlarini batafsil o'rganib chiqdilar. To'liq kirish / chiqish munosabatlari ko'rsatilishi mumkin. The aloqa matritsasi sinxron aloqa uchun protokol o'rnatadi. Buning afzalligi shundaki, u har bir mashinaning ishlashini ularning aloqasidan ajratib, har bir harakatni alohida sinovdan o'tkazishga imkon beradi. Ushbu kompozitsion model standartga teng ekanligi isbotlangan Stream X-Machine,[24] shuning uchun Holcombe va Ipate tomonidan ishlab chiqilgan oldingi sinov nazariyasidan foydalanish.

Ushbu X-machine varianti muhokama qilinadi batafsilroq alohida sahifada.

Ob'ekt X-Machine (OXM)

Kirill Bogdanov va Entoni Simons ob'ektga yo'naltirilgan tizimlarda ob'ektlarning xatti-harakatlarini modellashtirish uchun X-mashinaning bir nechta variantlarini ishlab chiqdilar.[25] Ushbu model farq qiladi Stream X-Machine monolitik ma'lumotlar turi X ning taqsimlanishi va ketma-ket tuzilgan bir nechta ob'ektlar tomonidan qamrab olinishi; va tizimlar kirish va chiqish orqali emas, balki usul chaqiruvlari va natijalar asosida boshqariladi. Ushbu sohadagi keyingi ishlar kengaytirilgan subklass ob'ektlarida superklassning holatini ajratib turadigan meros kontekstida rasmiy sinov nazariyasini moslashtirish bilan bog'liq.[26]

"CCS-kengaytirilgan X-mashina" (CCSXM) modeli keyinchalik Simons va Stannett tomonidan 2002 yilda asenkron aloqa mavjud bo'lganda ob'ektga yo'naltirilgan tizimlarning xulq-atvorini to'liq sinovdan o'tkazish uchun ishlab chiqilgan.[27] Buning o'xshashligi kutilmoqda NASA so'nggi taklif; ammo ikkita modelni aniq taqqoslash hali amalga oshirilmagan.

Shuningdek qarang

Yuklab olinadigan texnik hisobotlar

  • M. Stannett va A. J. X. Simons (2002) CCS-kengaytirilgan X-mashinalari yordamida ob'ektga yo'naltirilgan tizimlarning xulq-atvorini to'liq sinovdan o'tkazish. Tech Report CS-02-06, Sheffield University of Computer Science bo'limi, Sheffield universiteti. Yuklash
  • J. Aguado va A. J. Kovling (2002) Sinov uchun X-mashina nazariyasining asoslari. Tech Report CS-02-06, Sheffield University of Computer Science bo'limi, Sheffield universiteti. Yuklash
  • J. Aguado va A. J. Kovling (2002) Tarqatilgan tizimlarni aniqlash uchun X-mashinalarni aloqa qilish tizimlari. Tech Report CS-02-07, Sheffield University of Computer Science, Informatika bo'limi. Yuklash
  • M. Stannett (2005) X-mashinalari nazariyasi - 1-qism. Tech Report CS-05-09, Sheffield University of Computer Science, Informatika bo'limi. Yuklash

Tashqi havolalar

Adabiyotlar

  1. ^ a b S. Eilenberg (1974) Avtomatlar, tillar va mashinalar, jild. A. Academic Press, London.
  2. ^ M. Holcombe (1988) "X-mashinalar dinamik tizim spetsifikatsiyasi uchun asos", Dastur muhandisligi jurnali 3(2), 69-76 betlar.
  3. ^ M. Holcombe (1988) "Inson-mashina interfeysi spetsifikatsiyasining rasmiy usullari", Xalqaro J. Buyruq va nazorat, aloqa va ma'lumot. Tizimlar. 2, 24-34 betlar.
  4. ^ M. Holcombe (1986) 'Hujayra biokimyosining matematik modellari'. Texnik hisobot CS-86-4, Sheffield University of Computer Science, Informatika bo'limi.
  5. ^ M. Stannett (1987) "Buyruqlar tizimida qarorlarni qabul qilishga tashkiliy yondashuv." Xalqaro J. Buyruq va nazorat, aloqa va ma'lumot. Tizimlar. 1, 23-34 betlar.
  6. ^ a b Gilbert Laykok (1993) Texnik spetsifikatsiyaga asoslangan dasturiy ta'minotni sinash nazariyasi va amaliyoti. Sheffild universiteti nomzodlik dissertatsiyasi. Xulosa Arxivlandi 2007 yil 5-noyabr, soat Orqaga qaytish mashinasi
  7. ^ a b M. Holcombe va F. Ipate (1998) To'g'ri tizimlar - biznes jarayonining echimini yaratish. Springer, Amaliy hisoblash seriyalari.
  8. ^ A. Bell va M. Xolkom (1996) 'Uyali ishlov berishning hisoblash modellari', In Uyali va molekulyar biologik tizimlarda hisoblash, tahrir. M. Xolkom, R. Paton va R. Kutbertson, Singapur, Jahon ilmiy matbuoti.
  9. ^ a b M. G. Xinchey, C. A. Rouff, J. L. Rash va V. F. Truskovski (2005) "Intellektual to'dalar uchun integral rasmiy uslubning talablari", FMICS'05 materiallari, 2005 yil 5-6 sentyabr, Lissabon, Portugaliya. Hisoblash texnikasi assotsiatsiyasi, 125-133 betlar.
  10. ^ A. Kornai (2009) Leksik semantika algebrasi. 2009 yilgi yig'ilishida taqdim etilgan hujjat Til matematikasi bo'yicha topshiriq. C. Ebert, G. Jäger, J. Michaelis (tahr.) Proc. 11-chi Til matematikasi seminari (MOL11) Springer LNCS 6149 174-199 [1]
  11. ^ G. Huet va B. Razet (2008) "Relational Machines bilan hisoblash" qo'llanmasi ICON-da taqdim etilgan, 2008 yil dekabr, Poona. "Arxivlangan nusxa" (PDF). Arxivlandi asl nusxasi (PDF) 2015 yil 19 fevralda. Olingan 7 avgust, 2013.CS1 maint: nom sifatida arxivlangan nusxa (havola)
  12. ^ P. Goyal, G. Xuet, A. Kulkarni, P. Sharf, R. Bunker (2012) "Sanskritcha ishlov berish uchun tarqatilgan platforma" Proc. COLING 2012, 1011–1028 betlar [2]
  13. ^ M. Stannett (1990) 'X-mashinalari va to'xtash muammosi: super-Tyuring mashinasini yaratish'. Hisoblashning rasmiy jihatlari 2, 331-41-betlar.
  14. ^ B. J. Kopeland (2002) 'Giperkompyuterlash'. Aql va mashinalar 12, 461-502 betlar.
  15. ^ F. Ipate va M. Holcombe (1998) "Mashinalarning umumlashtirilgan texnik xususiyatlarini takomillashtirish va sinash usuli". Int. J. Komp. Matematika. 68, 197-219 betlar.
  16. ^ F. Ipate va M. Holcombe (1997) "Barcha xatolarni topganligi isbotlangan integratsiyalashgan sinov usuli", Xalqaro kompyuter matematikasi jurnali 63, 159-178 betlar.
  17. ^ J. Barnard, C. Teaker, J. Uitvort va M. Vudvord (1995) "Haqiqiy vaqtda tizimlarning rasmiy dizayni uchun real vaqtda aloqa qiluvchi X-mashinalari", DARTS '95 materiallari, Universite Libre, Bryussel, Belgiya, 2005 yil 9–11-noyabr
  18. ^ J. Barnard (1996) COMX: Communicating X-mashinalari yordamida kompyuter tizimlarini rasmiy loyihalashtirish metodologiyasi. Doktorlik dissertatsiyasi, Staffordshire universiteti.
  19. ^ A. Alderson va J. Barnard (1997) "Xavfsiz o'tishni ta'minlash to'g'risida", SOCTR / 97/01 texnik hisoboti, Staffordshire universiteti hisoblash maktabi. (Citeseer)
  20. ^ E. Kehris, G. Eleftherakis va P. Kefalas (2000) "Ayrim hodisalarni simulyatsiya dasturlarini modellashtirish va sinash uchun X-mashinalaridan foydalanish", Proc. Elektronlar, tizimlar, aloqa va kompyuterlar bo'yicha 4-jahon multikonferentsiyasi, Afina.
  21. ^ P. Kefalas, G. Eleftherakis va E. Kehris (2000) "X-apparatlar bilan aloqa qilish: katta tizimlarning modulli spetsifikatsiyasi uchun amaliy yondashuv", Texnik hisobot CS-09/00, informatika kafedrasi, Siti kolleji, Saloniki.
  22. ^ H. Georgesku va C. Vertan (2000) "X-mashinalar oqimini aloqa qilishda yangi yondashuv", Umumjahon kompyuter fanlari jurnali 6 (5), 490-502 betlar.
  23. ^ P. R. Bird va A. J. Kovling (1994) 'Aloqa mashinalari tarmog'idan foydalangan holda mantiqiy dasturlashni modellashtirish', Proc. Parallel va taqsimlangan ishlov berish bo'yicha 2-Euromicro seminari, Malaga, 1994 yil 26-28 yanvar, 156-161-betlar. Xulosa
  24. ^ T.Balanesku, A.J.Kovling, X.Gorjesku, M.George, M.Xolcombe va C.Vertan (1999) 'X-mashinalar tizimlari aloqa qilish X-mashinalaridan ortiq emas', Umumjahon kompyuter fanlari jurnali, 5 (9), 494-507 betlar.
  25. ^ A. J. H. Simons, K. E. Bogdanov va W. M. L. Holcombe (2001) "Ob'ektli mashinalar yordamida to'liq funktsional sinov", Texnik hisobot CS-01-18, kompyuter fanlari bo'limi, Sheffild universiteti
  26. ^ A. J. H. Simons (2006) "Xulq-atvorga mos keladigan ob'ekt turlari uchun regressiya sinovlari nazariyasi", Dasturiy ta'minotni sinovdan o'tkazish, tekshirish va ishonchlilik, 16 (3), John Wiley, 133-156 betlar.
  27. ^ M. Stannett va A. J. H. Simons (2002) 'CCS-kengaytirilgan X-mashinalari', Texnik hisobot CS-2002-04, informatika kafedrasi, Sheffild universiteti, Buyuk Britaniya.