MS, University of Cincinnati, 2022, Engineering and Applied Science: Electrical Engineering

This thesis deals with the use of formal methods to enhance the correctness of systems. We focus on Programmable Logic Controllers (PLCs) to be implemented in ladder logic. We derive a TLA+ model for a general ladder logic program. This will help not only in identifying faults in the system being designed but also in enhancing the prevention of design errors. We describe three systems to exhibit the extent to which TLA+, which is a formal specification language, is accurate in finding faults in the systems and rectifying them. The systems we examine include a dishwasher, an elevator system, and a door locking system. Formal methods such as TLA+ provide well-defined models against which the actual system can compared to check accuracy and consistency.

Committee: Carla Purdy Ph.D. (Committee Member); Badri Vellambi Ravisankar Ph.D. (Committee Member); Wen-Ben Jone Ph.D. (Committee Member) Subjects: Electrical Engineering

PhD, University of Cincinnati, 2021, 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.

Committee: 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) Subjects: Computer Engineering