College of Engineering

Department of Computer Engineering  / College of Engineering at University of Mosul discussed a master’s thesis on “Development of a Model-based Verification Approach for Reliable Digital Devices” for the student (Fayhaa Hmeedy Khlayef), supervised by Assist. Prof. Dr. Shawkat Sabah Khairallah on Monday, Oct 30, 2023.

The thesis dealt with designing a digital system at a high level in terms of reliability and making it more dependable. The first direction of this thesis was proving and verifying the safety-critical digital system that is compatible with the safety property, therefore our approach used two formal verification techniques which are the Simulink Design Verifier (SLDV) which is provided by MathWorks Simulink, and the NuSMV model checker. The verification model-based design (VMBD) approach in SLDV need for modeling the digital system and modeling the property. The property was formulated using Simulink blocks, and because of the capabilities that Simulink provided, MBD of the system can be created easily. Whereas the NuSMV need to use the temporal logic to formulate the required property and modeling the behaviour of the system in SMV language which is characterized by its accuracy in verification. The second direction focuses on how to make the system more dependable and work correctly even if a fault occurred during system operation at running time. The proposed hybrid fault tolerated TMR technique which was able to detect the type of fault if permanent or transient, and isolate the failure system and replace it with an operational spare.