Data model verification via theorem proving
- Degree Grantor:
- University of California, Santa Barbara. Computer Science
- Degree Supervisor:
- Tevfik Bultan
- Place of Publication:
- [Santa Barbara, Calif.]
- Publisher:
- University of California, Santa Barbara
- Creation Date:
- 2016
- Issued Date:
- 2016
- Topics:
- Computer science
- Keywords:
- Software analysis,
Web applications,
Data models, and
Verification - Genres:
- Online resources and Dissertations, Academic
- Dissertation:
- Ph.D.--University of California, Santa Barbara, 2016
- Description:
Software applications have moved from desktop computers onto the web. This is not surprising since there are many advantages that web applications provide, such as ubiquitous access and distributed processing power. However, these benefits come at a cost. Web applications are complex distributed systems written in multiple languages. As such, they are prone to errors at any stage of development, and difficult to verify, or even test. Considering that web applications store and manage data for millions (even billions) of users, errors in web applications can have disastrous effects.
In this dissertation, we present a method for verifying code that is used to access and modify data in web applications. We focus on applications that use frameworks such as Ruby on Rails, Django or Spring. These frameworks are RESTful, enforce the Model-View-Controller architecture, and use Object Relational Mapping libraries to manipulate data. We developed a formal model for data stores and data store manipulation, including access control. We developed a translation of these models to formulas in First Order Logic (FOL) that allows for verification of data model invariants using off-the-shelf FOL theorem provers. In addition, we developed a method for extracting these models from existing applications implemented in Ruby on Rails. Our results demonstrate that our approach is applicable to real world applications, it is able to discover previously unknown bugs, and it does so within minutes on commonly available hardware.
- Physical Description:
- 1 online resource (160 pages)
- Format:
- Text
- Collection(s):
- UCSB electronic theses and dissertations
- Other Versions:
- http://gateway.proquest.com/openurl?url_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation&res_dat=xri:pqm&rft_dat=xri:pqdiss:10194493
- ARK:
- ark:/48907/f3pr7w57
- ISBN:
- 9781369575842
- Catalog System Number:
- 990047511680203776
- Copyright:
- Ivan Bocic, 2016
- Rights:
In Copyright
- Copyright Holder:
- Ivan Bocic
File | Description |
---|---|
Access: Public access | |
Bocic_ucsb_0035D_13245.pdf | pdf (Portable Document Format) |