Geri Dön

An approach for automated verification of web applications using model checking and replaying the scenarios of counter example

Web uygulamalarının model denetleme kullanılarak otomatik doğrulanması ve karşı örnek senaryolarının oynatılması için bir yaklaşım

  1. Tez No: 409166
  2. Yazar: YUDUM PAÇİN
  3. Danışmanlar: DOÇ. AYSU BETİN CAN
  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: 2015
  8. Dil: İngilizce
  9. Üniversite: Orta Doğu Teknik Üniversitesi
  10. Enstitü: Enformatik Enstitüsü
  11. Ana Bilim Dalı: Bilişim Sistemleri Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. Sayfa Sayısı: 148

Özet

Web uygulamalarının kullanım alanının gittikçe artması, doğrulama yöntemlerinin önemini de arttırmaktadır. Bu çalışmada, model denetleme kullanılarak web uygulamalarının erişim kontrolü, bağlantı tutarlılığı ve erişilebilirlik özelliklerinin doğrulanması için bir yöntem öneriyoruz. Bu yaklaşımda, kullanıcılara sorgulanacak özellikleri ara yüz yardımıyla tanımlama imkanı verilmektedir. Sorgulanan özelliklerin ihlaline neden olan yürütme adımları, model denetleyicinin ürettiği karşı örneklerin web tarayıcısı üzerinde oynatılmasını sağlayan betiklere çevrilmektedir. Bu sayede, kullanıcıların web uygulamasında bulunan hatalı davranışları gözlemlemelerine olanak verilmekte, kullanıcıya model denetleme aracının ürettiği anlaşılması zor ve oldukça detaylı olan karşı örneklerin çözümlenmesinde yardımcı olunmaktadır. Buna ek olarak, doğrulama sürecini otomatikleştirmek için, model denetleme aracına girdi olarak belirlenen modelin web uygulamasından elde edilmesinin de otomatikleştirilmesi gerekmektedir. Biz bu amaçla, var olan iki dinamik web arama robotunu kullanmakta ve çıkan modelleri otomatik olarak kendi geliştirdiğimiz ara web modeline çevirmekteyiz. Bu ara web modeli, hem model çıkarma aracından bağımsızlık sağlamakta hem de doğrulama sürecinin kesinliğini arttırmak için kullanıcıya çıkan modeli manuel biçimde düzenleme imkanı sunmaktadır. Ayrıca, bu amaçla geliştirdiğimiz aracın değerlendirilmesi kapsamında bir kullanıcı çalışması yürütülmüştür. Katılımcılar, hata tespiti ve hataların görselleştirilmesini yararlı bulduklarını bildirmişlerdir. Ayrıca, aracın hata tespitindeki etkililiği gerçek web uygulamalarıyla değerlendirilmiş ve aracın hataları tespit edebildiği gözlemlenmiştir.

Özet (Çeviri)

The increase in the use of web applications in various domains, raised the importance of the methodologies for verification of web applications. We propose a framework for the verification of web applications with respect to access control, link consistency and reachability properties using model checking. In this approach, users define the properties by explanatory guidance of user interface. The execution traces that lead to a property violation is translated to a script that automates the replaying of the counterexample scenarios on a web browser. This facility enables the user to observe incorrect behaviors of the web application with respect to specified properties so that the user is released from the tedious task of understanding and interpreting the counterexamples generated by the model checker. In addition, to automate this verification process, we need to automate the model extraction of a web application to be given to the model checker as an input. To this purpose, we use two dynamic web application crawlers and automatically transform their models to an intermediate web model we have developed. This intermediate web model both enables model extraction tool independence and gives the user to edit the model manually to increase precision of verification process. In order to evaluate the tool we developed for this purpose, we conducted a user study and the participants reported our tool to be useful for detecting and visualizing errors. We also evaluated the effectiveness on real web applications and observed that the tool can reveal real faults.

Benzer Tezler

  1. A knowledge-based product line for semantic modeling of web service families

    Bilgi tabanlı anlamsal ağ servis ailesi modeli üretim bandı

    UMUT ORHAN

    Yüksek Lisans

    İngilizce

    İngilizce

    2009

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik Üniversitesi

    Bilgisayar Mühendisliği Bölümü

    DOÇ. DR. ALİ HİKMET DOĞRU

  2. Unconstrained face recognition under mismatched conditions

    Eşleşmeyen koşullar altında yüz tanıma

    OMID ABDOLLAHI AGHDAM

    Yüksek Lisans

    İngilizce

    İngilizce

    2018

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    DOÇ. DR. HAZIM KEMAL EKENEL

  3. Kıyı yapısı inşaatları için iş güvenliği risk yönetim sistemi

    Occupational safety risk management system for coastal structure construction

    DİNÇER İNANÇ YILMAZ

    Doktora

    Türkçe

    Türkçe

    2024

    Mühendislik Bilimleriİstanbul Teknik Üniversitesi

    İnşaat Mühendisliği Ana Bilim Dalı

    DOÇ. DR. DENİZ ARTAN

  4. Development of a library for automated verification of UML models

    UML modellerinin otomatik olarak doğrulanmasını sağlayan bir kütüphane geliştirilmesi

    MAKBULE FİLİZ ÇELİK

    Yüksek Lisans

    İngilizce

    İngilizce

    2006

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik Üniversitesi

    Bilişim Sistemleri Ana Bilim Dalı

    DR. ALTAN KOÇYİĞİT

  5. Architecture of constraints: A mass customization oriented approach for housing design

    Kısıtlarla tanımlanan mimarlık: Kitlesel özelleştirme odaklı konut tasarımı

    BENGİSU İLKSOY

    Yüksek Lisans

    İngilizce

    İngilizce

    2015

    Mimarlıkİstanbul Teknik Üniversitesi

    Mimarlık Ana Bilim Dalı

    DOÇ. DR. MİNE ÖZKAR KABAKÇIOĞLU