A Global Review of Publicly Available Datasets Containing Fundus Images: Characteristics, Barriers to Access, Usability, and Generalizability.

This article provides a comprehensive and up-to-date overview of the repositories that contain color fundus images. We analyzed them regarding availability and legality, presented the datasets' characteristics, and identified labeled and unlabeled image sets. This study aimed to complete all publicly available color fundus image datasets to create a central catalog of available color fundus image datasets.

Deceptive Tricks in Artificial Intelligence: Adversarial Attacks in Ophthalmology.

The artificial intelligence (AI) systems used for diagnosing ophthalmic diseases have significantly progressed in recent years. The diagnosis of difficult eye conditions, such as cataracts, diabetic retinopathy, age-related macular degeneration, glaucoma, and retinopathy of prematurity, has become significantly less complicated as a result of the development of AI algorithms, which are currently on par with ophthalmologists in terms of their level of effectiveness. However, in the context of building AI systems for medical applications such as identifying eye diseases, addressing the challenges of safety and trustworthiness is paramount, including the emerging threat of adversarial attacks. Research has increasingly focused on understanding and mitigating these attacks, with numerous articles discussing this topic in recent years. As a starting point for our discussion, we used the paper by Ma et al. "Understanding Adversarial Attacks on Deep Learning Based Medical Image Analysis Systems". A literature review was performed for this study, which included a thorough search of open-access research papers using online sources (PubMed and Google). The research provides examples of unique attack strategies for medical images. Unfortunately, unique algorithms for attacks on the various ophthalmic image types have yet to be developed. It is a task that needs to be performed. As a result, it is necessary to build algorithms that validate the computation and explain the findings of artificial intelligence models. In this article, we focus on adversarial attacks, one of the most well-known attack methods, which provide evidence (i.e., adversarial examples) of the lack of resilience of decision models that do not include provable guarantees. Adversarial attacks have the potential to provide inaccurate findings in deep learning systems and can have catastrophic effects in the healthcare industry, such as healthcare financing fraud and wrong diagnosis.

Bounded Model Checking for Metric Temporal Logic Properties of Timed Automata with Digital Clocks.

Metric temporal logic (MTL) is a popular real-time extension of linear temporal logic (LTL). This paper presents a new simple SAT-based bounded model-checking (SAT-BMC) method for MTL interpreted over discrete infinite timed models generated by discrete timed automata with digital clocks. We show a new translation of the existential part of MTL to the existential part of linear temporal logic with a new set of atomic propositions and present the details of the new translation. We compare the new method's advantages to the old method based on a translation of the hard reset LTL (HLTL). Our method does not need new clocks or new transitions. It uses only one path and requires a smaller number of propositional variables and clauses than the HLTL-based method. We also implemented the new method, and as a case study, we applied the technique to analyze several systems. We support the theoretical description with the experimental results demonstrating the method's efficiency.

SAT and SMT-Based Verification of Security Protocols Including Time Aspects.

For many years various types of devices equipped with sensors have guaranteed proper work in a huge amount of machines and systems. For the proper operation of sensors, devices, and complex systems, we need secure communication. Security protocols (SP) in this case, guarantee the achievement of security goals. However, the design of SP is not an easy process. Sometimes SP cannot realise their security goals because of errors in their constructions and need to be investigated and verified in the case of their correctness. Now SP uses often time primitives due to the necessity of security dependence on the passing of time. In this work, we propose and investigate the SAT-and SMT-based formal verification methods of SP used in communication between devices equipped with sensors. For this, we use a formal model based on networks of communicating timed automata. Using this, we show how the security property of SP dedicated to the sensors world can be verified. In our work, we investigate such timed properties as delays in the network and lifetimes. The delay in the network is the lower time constraint related to sending the message. Lifetime is an upper constraint related to the validity of the timestamps generated for the transmitted messages.