Geri Dön

Tool support for qualitative reasoning in event-B

Başlık çevirisi mevcut değil.

  1. Tez No: 400168
  2. Yazar: EMRE YILMAZ
  3. Danışmanlar: DR. THAİ SON HOANG, PROF. DR. DAVİD BASİN
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2010
  8. Dil: İngilizce
  9. Üniversite: Eidgenössische Technische Hochschule Zürich (ETH)
  10. Enstitü: Yurtdışı Enstitü
  11. Ana Bilim Dalı: Belirtilmemiş.
  12. Bilim Dalı: Belirtilmemiş.
  13. Sayfa Sayısı: 86

Özet

Özet yok.

Özet (Çeviri)

Event-B is a notation and method for modelling discrete transition systemsby renement. The standard reasoning in Event-B is based on nondeterminism,however some system behaviours are more appropriately modelledprobabilistically. Earlier work has extended Event-B with means forreasoning about qualitative probability. The extension provides proof obligationsto prove almost-certain termination of systems and does not complicatethe existing Event-B notation or method. However, this early work does notmention the preservation of qualitative reasoning in the case of renement.Within our work we discuss how qualitative probabilistic reasoning can bemaintained during renement and propose some restrictions and conditionsfor almost-certain termination on renement.We continue the above investigation with the integration of qualitative probabilisticreasoning into Event-B further towards the direction of having a toolsupport. We extend the Rodin Platform to support proving almost-certaintermination and using our new developed tool support we model some examplealgorithms terminating almost-certainly. In passing by, we formalise anon-trivial algorithm, namely Rabin's choice coordination. Our correctnessreasoning is a combination of termination proofs in terms of probabilisticconvergence and standard invariants techniques with renement. We usethe technique of splitting/merging the events to avoid having complicatedproofs.

Benzer Tezler

  1. Çok ölçütlü sorun çözümüne yönelik bir bütünleşik karar destek modeli

    Integrated decision aid model for multiattribute problem solving

    YUSUF İLKER TOPÇU

    Doktora

    Türkçe

    Türkçe

    2000

    Endüstri ve Endüstri Mühendisliğiİstanbul Teknik Üniversitesi

    PROF. DR. FÜSUN ÜLENGİN

  2. Matematik okuryazarlığının problem çözmede sistematik çeşitleme ile desteklenmesinin öğretim deneyi yoluyla incelenmesi

    Investigation of supporting mathematical literacy through systematic variation problems via teaching experiment

    FATMA KIZILTOPRAK

    Doktora

    Türkçe

    Türkçe

    2017

    Eğitim ve ÖğretimAnadolu Üniversitesi

    Matematik Eğitimi Ana Bilim Dalı

    DOÇ. DR. TANGÜL KABAEL

  3. Okul öncesi öğretmenlerinin sınıf içi soru sorma faaliyetlerine yönelik pedagojik inanç sistemleri ve kavramları

    Pedagogical belief systems and concepts regarding the in-class questioning activities of preschool teachers

    KÜBRA CERGİBOZAN

    Yüksek Lisans

    Türkçe

    Türkçe

    2022

    Eğitim ve Öğretimİstanbul Aydın Üniversitesi

    Temel Eğitim Ana Bilim Dalı

    DOÇ. DR. YILMAZ SOYSAL

  4. İstanbul-Paşaköy-B.Bakkalköy arası enerji nakil hattı kamulaştırma bilgi sistemi pilot çalışması

    Başlık çevirisi yok

    NURAY BAŞ

    Yüksek Lisans

    Türkçe

    Türkçe

    1998

    Jeodezi ve Fotogrametriİstanbul Teknik Üniversitesi

    Jeodezi ve Fotogrametri Mühendisliği Ana Bilim Dalı

    DOÇ. DR. GONCA COŞKUN

  5. Simulator-based evaluation of human response in emergencies

    Acil durumlarda ınsan faktörünün simülatör ortamında değerlendirilmesi

    ESMA UFLAZ

    Doktora

    İngilizce

    İngilizce

    2023

    Denizcilikİstanbul Teknik Üniversitesi

    Deniz Ulaştırma Mühendisliği Ana Bilim Dalı

    Prof. Dr. ÖZCAN ARSLAN