დაწყების თარიღი: 2015-03-05 დასრულების თარიღი: 2018-03-05
წვდომის კონტროლი უსაფრთხო კომპიუტერული სისტემების აგების ცენტრალური საკითხია. იგი განსაზღვრულია, როგორც გარკვეული სუბიექტისთვის გარკვეულ
ობიექტზე წვდომის ნებართვის მიცემის ან არმიცემის უნარი, რომელმაც უნდა უზრუნველყოს შესაბამის კომპიუტერულ რესურსთან დაკავშირებული ინფორმაციის
კონფიდენციალურობა, რესურსის მთლიანობა და ავტორიზებული სუბიექტებისთვის მისი მისაწვდომობა. გამოყენების კონტროლი ამ პრობლემისადმი ახალი,
თანამედროვე მიდგომაა, რომელიც მართავს წვდომას ღია, ჰეტროგენულ ქსელებთან დაკავშირებულ კომპიუტერულ გარემოში. პროექტის მიზანი იყო გამოყენების
კონტროლისთვის ისეთი ფორმალური სტრუქტურის შემოთავაზება, რომელსაც შეეძლებოდა გამოყენების კონტროლის მთავარი მოდელების ადეკვატური
ფორმალიზაცია და შესაფერისი იქნებოდა მათი ანალიზისა და ვერიფიკაციისთვის. ამისათვის ავირჩიეთ გადაწერის თეორია, კონკრეტულად, ρLog აღრიცხვა,
რომელიც აფართოებს ლოგიკურ პროგრამებს მათში პირობებიანი, სტრატეგიებით მართული გადაწერის წესების დაშვებით, შევადარეთ იგი გადაწერის ცნობილ
ფორმალიზმებს და ვაჩვენეთ კავშირი კონტროლის მოთხოვნებს და გადაწერის თვისებებს შორის. გარდა ამისა, ერთ-ერთი ასეთი თვისება, კონფლუენტურობა,
დეტალურად შევისწავლეთ თარგთა აღრიცხვის ვარიანტისთვის, რომელიც აზოგადებს გადაწერის ჩვენთვის საჭირო ფორმალიზმებს.