A Hybrid Deep Learning and Model-Checking Framework for Accurate Brain Tumor Detection and Validation

Model checking is an automatic technique for verifying the correctness properties of safety-critical reactive systems. This method has been successfully applied to find subtle errors in complex systems. Model checking techniques have a wide range of application domains, among which large-scale distributed systems [1-3], signal [4], and medical images analysis [5-8]. The research related to the last topic is still ongoing looking for the perfect (precise, complete, simple) approach for analyzing medical images. The use of model checking is relatively recent, in particular regarding the verification of the analysis of medical images. In this domain, model checking in medical images has shown to be a promising application that can significantly facilitate the work of professionals. What motivates us in this study, considering that model checking is increasingly used in testing to check whether a system model satisfies a property, is to take model checking in its usual role to take on more advanced roles in medical image analysis by applying model-checking logic to medical images and detection of tumors in addition to validation of properties through tests or case studies.