ROS Theses Repository

View Item 
  •   ROS Home
  • Textiles & Design
  • Doctoral Theses (Textiles & Design)
  • View Item
  •   ROS Home
  • Textiles & Design
  • Doctoral Theses (Textiles & Design)
  • View Item
  •   ROS Home
  • Textiles & Design
  • Doctoral Theses (Textiles & Design)
  • View Item
  • Admin
JavaScript is disabled for your browser. Some features of this site may not work without it.

Model checking web applications

View/Open
AlzahraniMY_1215_macs.pdf (1.566Mb)
Date
2015-12
Author
Alzahrani, Mohammed Yahya
Metadata
Show full item record
Abstract
The modelling of web-based applications can assist in capturing and understanding their behaviour. The development of such applications requires the use of sound methodologies to ensure that the intended and actual behaviour are the same. As a verification technique, model checking can assist in finding design flaws and simplifying the design of a web application, and as a result the design and the security of the web application can be improved. Model checking has the advantage of using an exhaustive search of the state space of a system to determine if the specifications are true or not in a given model. In this thesis we present novel approaches in modelling and verifying web applications' properties to ensure their design correctness and security. Since the actions in web applications rely on both the user input and the server status; we propose an approach for modelling and verifying dynamic navigation properties. The Spin model checker has been used successfully in verifying communication protocols. However, the current version of Spin does not support modelling time. We integrate discrete time in the Spin model to allow the modelling of realistic properties that rely on time constraints and to analyse the sequence of actions and time. Examining the sequence of actions in web applications assists in understanding their behaviour in different scenarios such as navigation errors and in the presence of an intruder. The model checker Uppaal is presented in the literature as an alternative to Spin when modelling real-time systems. We develop models with real time constraints in Uppaal in order to validate the results from the Spin models and to compare the differences between modelling with real time and with discrete time as in Spin. We also compare the complexity and expressiveness of each model checker in verifying web applications' properties. The web application models in our research are developed gradually to ensure their correctness and to manage the complexities of specifying the security and navigation properties. We analyse the compromised model to compare the differences in the sequence of actions and time with the secure model to assist in improving early detections of malicious behaviour in web applications.
URI
http://hdl.handle.net/10399/3024
Collections
  • Doctoral Theses (Textiles & Design)

Browse

All of ROSCommunities & CollectionsBy Issue DateAuthorsTitlesThis CollectionBy Issue DateAuthorsTitles

ROS Administrator

LoginRegister
©Heriot-Watt University, Edinburgh, Scotland, UK EH14 4AS.

Maintained by the Library
Tel: +44 (0)131 451 3577
Library Email: libhelp@hw.ac.uk
ROS Email: open.access@hw.ac.uk

Scottish registered charity number: SC000278

  • About
  • Copyright
  • Accessibility
  • Policies
  • Privacy & Cookies
  • Feedback
AboutCopyright
AccessibilityPolicies
Privacy & Cookies
Feedback
 
©Heriot-Watt University, Edinburgh, Scotland, UK EH14 4AS.

Maintained by the Library
Tel: +44 (0)131 451 3577
Library Email: libhelp@hw.ac.uk
ROS Email: open.access@hw.ac.uk

Scottish registered charity number: SC000278

  • About
  • Copyright
  • Accessibility
  • Policies
  • Privacy & Cookies
  • Feedback
AboutCopyright
AccessibilityPolicies
Privacy & Cookies
Feedback