Үлестiрiлген алгоритмдер және оларды Byzantine моделдi тексерiс арқылы верификациялау
Кілт сөздер:
үлестiрiлген алгоритмдер, паралелльдi программа, ByMC, модельдi тексерiс, верификацияАңдатпа
Жүйенiң әрбiр алгоритмдерi сенiмдi үлестiрiлген жүйелердi құруда негiзгi түйiндерi болып табылады. Бұл алгоритмдер жүйенiң сенiмдi болуына кепiлдiк беру үшiн, бiз осы алгоритмдер дұрыс жұмыс жасауына кепiлдiк беруiмiз қажет. Алайда, бекемдiкпен негiзделген үлестiрiлген алгоритмдерге моделдi тексерiс орындау тек кiшiгiрiм жүйелер үшiн ғана болуы мәлiм [1]. Соңғы нәтижесiнде, үлкен жүйедегi бекемделген үлестiрiлген алгоритмдердi автоматты түрде тексеру қажет. Бұл есептеу жүйелерiнiң сенiмдiлiгiн арттыруға бағытталғандықтан ол алгоритмдер талаптарына сай дұрыс жұмысын жасауы өте маңызды. Әр түрлi детерминисттiк емес түйiндерi үшiн темпоралды деңгейде үлестiрiлген алгоритмдердiң корректiлiк аргументiнде қате кету өте оңай болмақ. Сондықтан олар модель тексеруге сенiмдi материалдар бола алмайды. Алайда, үлестiрiлген алгоритмдердiң сенiмдiлiгiне модельдi тексеру әдiсi өте қиын. Бұл мақалада, Spin және ByMC (Byzantine Model Checker [3]) көмегiмен "Parsing"алгоритмiн Broadcast хабар таратушы [2] әдiсiмен моделдеп тексеруiн қарастырамыз. Ұсынылатын LTL(Linear-temporal logic) қасиеттер қауiпсiздiк және өмiрсүргiштiк.
