Repair of timed automata for non-vacuous satisfaction of requirements
Zamanlı otomatların gerekliliklerin anlamlı sağlanması için tamiri
- Tez No: 831587
- Danışmanlar: DOÇ. DR. EBRU AYDIN GÖL
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2023
- Dil: İngilizce
- Üniversite: Orta Doğu Teknik Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 46
Özet
Biçimsel doğrulama alanında zamanlı otomatlar gerçek-zamanlı sistemleri ve onların gerekliliklerini doğrulamak için kullanılabilir. Bir sistemi zamanlı otomat kullanarak modellemek, o sistem üzerinde biçimsel doğrulama yöntemleri kullanarak o model üzerinde belli özelliklerin varlığını veya yokluğunu incelemeyi mümkün kılar. Bu özelliklerden birisi de anlamsızlıktır. Basitçe anlamsızlık, bir gereksinim kümesinin mantıksal değerlemesini değiştirmeden daha basit bir karşılığıyla değiştirilebilecek bir gereksinim altkümesinin varlığıdır. Bu tezde, zamanlı otomatlarla temsil edilen bir gereksinim kümesindeki anlamsızlığın sebeplerini bulan ve bunları çözerek anlamsızlığı tamir eden iki algoritma sunulmuştur.
Özet (Çeviri)
In the field of formal verification, timed automata are used to formalize real-time systems and their requirements. Modeling a system with a timed automaton enables the use of formal methods to analyze the model for the existence or lack of certain characteristics. One such characteristic is the property of vacuity. In simplified terms, vacuity is the existence of a subset of the requirements which can be replaced with a simpler counterpart without altering the logical valuation of the set of the requirements. In this thesis, we propose algorithms to identify and remove causes of vacuity from timed automata so that the resulting automata will not be vacuous.
Benzer Tezler
- Models of synchronous production lines with no intermediate buffers
Ara stoksuz eş zamanlı üretim hattı modelleri
HANDE ÇETİNAY
Yüksek Lisans
İngilizce
2010
Endüstri ve Endüstri MühendisliğiOrta Doğu Teknik ÜniversitesiEndüstri Mühendisliği Bölümü
PROF. DR. SENCER YERALAN
PROF. DR. SİNAN KAYALIGİL
- MEDEMAS-Medical device maintenance management system via remote access
MEDEMAS-uzaktan erişimle tıbbi cihaz bakım yönetim sistemi
ÜLKÜ BALCI DOĞAN
Yüksek Lisans
İngilizce
2010
BiyomühendislikBoğaziçi ÜniversitesiBiyomedikal Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMED ÖZKAN
- Demir ve çelik tesislerinde bakım uygulamaları
The Maintenance applications in iron and steel industry
M.OĞUZ KARTEPE
Yüksek Lisans
Türkçe
1991
Endüstri ve Endüstri Mühendisliğiİstanbul Teknik ÜniversitesiPROF.DR. MUSTAFA SAVCI
- Multipl skleroz hastalarında repetetif transkraniyal manyetik stimülasyonun spastisite, özürlülük, yorgunluk, kognisyon, yaşam kalitesi ve serum nörofilaman hafif zincir düzeyi üzerine etkisinin değerlendirilmesi
Efficacy of repetitive transcranial magnetic stimulation on spasticity, disability, fatigue, cognition, quality of life and serum neurofilament light chain level in multiple sclerosis patients
REZZAN YILDIZ
Tıpta Uzmanlık
Türkçe
2023
NörolojiAnkara Yıldırım Beyazıt ÜniversitesiNöroloji Ana Bilim Dalı
DOÇ. DR. MEHMET İLKER YÖN
- Eğitim binalarının onarım işlerinin zaman ve bütçe açısından incelenmesi
Examination of repair works of educational buildings in terms of time and budget
KERİM BURAK CANBAY
Yüksek Lisans
Türkçe
2022
İnşaat Mühendisliğiİstanbul Gedik Üniversitesiİnşaat Mühendisliği Ana Bilim Dalı
DR. ÖĞR. ÜYESİ GÖKHAN KAZAR