Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


38273.pdf (6.32 MB)

ETD Abstract Container

Abstract Header

Using Formal Methods to Build and Validate Reliable and Secure Smart Systems via TLA+

Obeidat, Nawar H.
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1623169331790079

Abstract Details

2021, PhD, University of Cincinnati, Engineering and Applied Science: Computer Science and Engineering.
Verification and validation are very important in the design of any system. For safety-critical systems, especially, the validation level is crucial. In this work, developing a robust procedure for designing smart, safe, secure systems is our eventual goal. There are different methods for verification and validation, but formal methods are used widely to validate these systems due to their high level of confidence for guaranteeing correctness, security, and safety properties. TLA+ is a formal specification language and its TLC model checker will be used in this work to formally verify and validate several example systems, and to find security hacks. Designing smart systems has recently received much attention because of the ability to connect heterogeneous sub-systems together to build a fully controlled smart system. Here we propose models for three systems: a smart school building system, an ADS-B system for avionics, and a SCADA system. We model the systems using UML diagrams to describe objects, states, and sequences of actions. Formal methods techniques are used to verify the properties of the systems. TLA+ is used for formal modeling. For the smart school building system, the ADS-B system, and the SCADA system, we verify their properties and correctness using the TLA+ toolbox and the TLC model checker. Also, we use the TLC model checker to find example security bugs we introduce into the designs.
Carla Purdy, Ph.D. (Committee Chair)
Shaaban Abdallah, Ph.D. (Committee Member)
Nan Niu, Ph.D. (Committee Member)
Massoud (Max) Rabiee, Ph.D. (Committee Member)
Boyang Wang (Committee Member)
143 p.
Computer Engineering
TLA; Formal Methods; Verification and Validation; Smart Systems; Safety; Security

Recommended Citations

Citations

  • Obeidat, N. H. (2021). Using Formal Methods to Build and Validate Reliable and Secure Smart Systems via TLA+ [Doctoral dissertation, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1623169331790079

    APA Style (7th edition)

  • Obeidat, Nawar. Using Formal Methods to Build and Validate Reliable and Secure Smart Systems via TLA+. 2021. University of Cincinnati, Doctoral dissertation. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ucin1623169331790079.

    MLA Style (8th edition)

  • Obeidat, Nawar. "Using Formal Methods to Build and Validate Reliable and Secure Smart Systems via TLA+." Doctoral dissertation, University of Cincinnati, 2021. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1623169331790079

    Chicago Manual of Style (17th edition)

ucin1623169331790079
410
© 2021, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.