Analyzing synchronization objects using theprocess algebra CSP and its model checker FDR
Proses cebiri CSP ve model denetleyicisi FDRkullanarak senkronizasyon nesnelerinin analizi
- Tez No: 918121
- Danışmanlar: PROF. DR. GAVIN LOWE
- Tez Türü: Yüksek Lisans
- Konular: Matematik, Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Mathematics, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2023
- Dil: İngilizce
- Üniversite: Unıversıty Of Oxford
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Matematik ve Bilgisayar Bilimleri Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: Belirtilmemiş.
Özet
Senkronizasyon nesneleri, concurrent (eşzamanlı) programlarda kullanılan senkronizasyon aracılarıdır: Başka iş parçacıkları belirli bir senkronizasyon noktasına ulaşana kadar iş parçacıklarını bloke ederler ve ancak o zaman devam etmelerine izin verirler. Örneğin bir senkron kanal, bir gönderici ve bir alıcı arasında veri iletmek için kullanılır ve her ikisi de diğeri hazır oluncaya kadar bloke olur. Bir başka yaygın örnek olan bariyer, bir concurrent (eşzamanlı) programdaki tüm iş parçacıkları arasında global senkronizasyon sağlamak için kullanılır, yani tüm iş parçacıkları hazır olmadan önce hiçbir iş parçacığı işleme devam edemez. Senkronizasyon doğrusallaştırılabilirliği, senkronizasyonların katılımcı iş parçacıklarının ilgili işlemlerinin çağrılması ve geri dönüşü arasında atomik olarak gerçekleşmesi gerektiğini belirten bir güvenlik özelliğidir. Senkronizasyon ilerleyebilirliği, bir senkronizasyona katılabilecek bekleyen çağrılar olduğunda, sonunda bir senkronizasyonun gerçekleşeceğini ve katılımcı çağrıların sonunda geri döneceğini belirten bir ilerleme özelliğidir. Bu raporda, çeşitli senkronizasyon nesnelerinin önerilen gerçeklemelerinin senkronizasyon doğrusallaştırılabilirliğinin ve senkronizasyon ilerleyebilirliğinin biçimsel doğrulamasını (formal verification) yapıyoruz. İlk olarak proses cebiri CSP'yi kullanarak gerçeklemeyi modelliyor ve ardından istenen davranışı yakalayan onaylama süreçlerini (assertions) kontrol etmek için model denetleyicisi FDR'yi kullanıyoruz. Yaklaşımımızın güçlü ve zayıf yönlerini açıkça ortaya koyuyoruz. Ayrıca analizimizi geliştirmenin probleme özgü yollarını da gösteriyoruz.
Özet (Çeviri)
Synchronization objects are mediators of synchronization in concurrent programs: They block threads until some other threads reach a certain synchronization point and only then, they allow them to continue. A synchronous channel, for example, is used to transmit data between a sender and a receiver where both of them block until the other becomes available. A barrier, another common example, is used to achieve global synchronization between all threads in a concurrent program, i.e. no thread can proceed before all threads are available. Synchronization linearizability is a safety property that states synchronizations must appear to take place atomically between the invocation and return of participating threads' respective operations. Synchronization progressability is a progress property that states whenever there are pending invocations that can participate in a synchronization, a synchronization eventually takes place and participating invocations eventually return. In this report, we formally verify synchronization linearizability and synchronization progressability of proposed implementations of various synchronization objects. We first model the implementation using the process algebra CSP and then use its model checker FDR to check assertions capturing desired behaviour. We make strengths and weaknesses of our approach clear. We also demonstrate problem-specific ways of improving our analysis.
Benzer Tezler
- Federe öğrenme kullanılarak nesnelerin interneti (IOT) verileri analizi
Analyzing internet of things (IOT) data using federated learning
SÜLEYMAN BURAK ALTINIŞIK
- DNS big data processing for detecting customersbehaviour of isp using an optimized apache spark cluster
İSP müşterilerin davranışlarını tespiti için optimize edilmiş bir apache spark kümesi kullanarak dns büyük veri işleme
YOUSEF ALKHANAFSEH
Yüksek Lisans
İngilizce
2022
İstanbul Teknik ÜniversitesiElektrik ve Elektronik Mühendisliği Ana Bilim Dalı
Yükleniyor...
- Zafiyet veritabanlarına göre trafo merkezlerindeki akıllı elektronik cihazların firmware analizörü
Firmware analyzer of intelligent electronic devices in substations based on vulnerability databases
KHOULOUD GARGOURI
- RF tabanlı hedef konumlandırma sistemleri
RF based target positioning systems
MAHMUT GÜLNAZ
Yüksek Lisans
Türkçe
2016
Hacettepe ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
Yükleniyor...
- Nonlinear dynamic analysis of eeg-signals using synchronization techniques
Eeg sinyallerinin senkronizasyon teknikleri kullanılarak doğrusal olmayan dinamik analizi
ALİ EED MOHAMMAD OLAMAT
Doktora
İngilizce
2019
İstanbul Üniversitesi-CerrahpaşaBiyomedikal Mühendisliği Ana Bilim Dalı
Yükleniyor...