Mark Lawford

Sajid Rahim, Kourosh Sabri, Anna Ells et al.

Retinopathy of Prematurity (ROP) is a potentially blinding eye disorder because of damage to the eye's retina which can affect babies born prematurely. Screening of ROP is essential for early detection and treatment. This is a laborious and manual process which requires trained physician performing dilated ophthalmological examination which can be subjective resulting in lower diagnosis success for clinically significant disease. Automated diagnostic methods can assist ophthalmologists increase diagnosis accuracy using deep learning. Several research groups have highlighted various approaches. Captured ROP Retcam images suffer from poor quality. This paper proposes the use of improved novel fundus preprocessing methods using pretrained transfer learning frameworks to create hybrid models to give higher diagnosis accuracy. Once trained and validated, the evaluations showed that these novel methods in comparison to traditional imaging processing contribute to better and in many aspects higher accuracy in classifying Plus disease, Stages of ROP and Zones in comparison to peer papers.

Federico Formica, Andrea Rota, Aurora Francesca Zanenga et al.

Deep Neural Networks (DNNs) are widely used by engineers to solve difficult problems that require predictive modeling from data. However, these models are often massive, with millions or billions of parameters, and require substantial computational power, RAM, and storage. This becomes a limitation in practical scenarios where strict size and resource constraints must be respected. In this paper, we present a novel concept-based pruning technique for DNNs that guides pruning decisions using human-interpretable concepts, such as features, colors, and classes. This is particularly important in a software engineering context, as DNNs are integrated into systems and must be pruned according to specific system requirements. Our concept-based pruning solution analyzes neuron activations to identify important neurons from a system requirements viewpoint and uses this information to guide the DNN pruning. We assess our solution using the VGG-19 network and a dataset of 26'384 RGB images, focusing on its ability to produce small, effective pruned DNNs and on the computational complexity and performance of these pruned DNNs. We also analyzed the pruning efficiency of our solution and compared alternative configurations. Our results show that concept-based pruning efficiently generates much smaller, effective pruned DNNs. Pruning greatly improves the computational efficiency and performance of DNNs, properties that are particularly useful for practical applications with stringent memory and computational time constraints. Finally, alternative configuration options enable engineers to identify trade-offs adapted to different practical situations.

Federico Formica, Stefano Gregis, Andrea Rota et al.

Recent Deep Neural Networks (DNN) applications ask for techniques that can explain their behavior. Existing solutions, such as Feature Guided Analysis (FGA), extract rules on their internal behaviors, e.g., by providing explanations related to neurons activation. Results from the literature show that these rules have considerable precision (i.e., they correctly predict certain classes of features), but the recall (i.e., the number of situations these rule apply) is more limited. To mitigate this problem, this paper presents Ensembles-based Feature Guided Analysis (EFGA). EFGA combines rules extracted by FGA into ensembles. Ensembles aggregate different rules to increase their applicability depending on an aggregation criterion, a policy that dictates how to combine rules into ensembles. Although our solution is extensible, and different aggregation criteria can be developed by users, in this work, we considered three different aggregation criteria. We evaluated how the choice of the criterion influences the effectiveness of EFGA on two benchmarks (i.e., the MNIST and LSC datasets), and found that different aggregation criteria offer alternative trade-offs between precision and recall. We then compare EFGA with FGA. For this experiment, we selected an aggregation criterion that provides a reasonable trade-off between precision and recall. Our results show that EFGA has higher train recall (+28.51% on MNIST, +33.15% on LSC), and test recall (+25.76% on MNIST, +30.81% on LSC) than FGA, with a negligible reduction on the test precision (-0.89% on MNIST, -0.69% on LSC).

Federico Formica, Stefano Gregis, Aurora Francesca Zanenga et al.

Understanding why neural networks make certain decisions is pivotal for their use in safety-critical applications. Feature-Guided Analysis (FGA) extracts slices of neural networks relevant to their tasks. Existing feature-guided approaches typically monitor the activation of the neural network neurons to extract the relevant rules. Preliminary results are encouraging and demonstrate the feasibility of this solution by assessing the precision and recall of Feature-Guided Analysis on two pilot case studies. However, the applicability in industrial contexts needs additional empirical evidence. To mitigate this need, this paper assesses the applicability of FGA on a benchmark made by the MNIST and LSC datasets. We assessed the effectiveness of FGA in computing rules that explain the behavior of the neural network. Our results show that FGA has a higher precision on our benchmark than the results from the literature. We also evaluated how the selection of the neural network architecture, training, and feature selection affect the effectiveness of FGA. Our results show that the selection significantly affects the recall of FGA, while it has a negligible impact on its precision.

Mehrnoosh Askarpour, Alan Wassyng, Mark Lawford et al.

Machine learning (ML) is finding its way into safety-critical systems (SCS). Current safety standards and practice were not designed to cope with ML techniques, and it is difficult to be confident that SCSs that contain ML components are safe. Our hypothesis was that there has been a rush to deploy ML techniques at the expense of a thorough examination as to whether the use of ML techniques introduces safety problems that we are not yet adequately able to detect and mitigate against. We thus conducted a targeted literature survey to determine the research effort that has been expended in applying ML to SCS compared with that spent on evaluating the safety of SCSs that deploy ML components. This paper presents the (surprising) results of the survey.

Guy Meyer, Alan Wassyng, Mark Lawford et al.

A sudden reliance on the internet has resulted in the global standardization of specific software and interfaces tailored for the average user. Whether it be web apps or dedicated software, the methods of interaction are seemingly similar. But when the computer tool is presented with unique users, specifically with a disability, the quality of interaction degrades, sometimes to a point of complete uselessness. This roots from one's focus on the average user rather than the development of a platform for all (a golden standard). This paper reviews published works and products that deal with providing accessibility to visually impaired online users. Due to the variety of tools that are available to computer users, the paper focuses on search engines as a primary tool for browsing the web. By analyzing the attributes discussed below, the reader is equipped with a set of references for existing applications, along with practical insight and recommendations for accessible design. Finally, the necessary considerations for future developments and summaries of important focal points are highlighted.

Monika Jaskolka, Vera Pantelic, Alan Wassyng et al.

Model-Based Development (MBD) is widely used for embedded controls development, with Matlab Simulink being one of the most used modelling environments in industry. As with all software, Simulink models are subject to evolution over their lifetime and must be maintained. Modularity is a fundamental software engineering principle facilitating the construction of complex software, and is used in textual languages such as C. However, as Simulink is a graphical modelling language, it is not currently well understood how modularity can be leveraged in development with Simulink, nor whether it can be supported with current Simulink modelling constructs. This paper presents an effective way of achieving modularity in Simulink by introducing the concept of a Simulink module. The effectiveness of the approach is measured using well-known indicators of modularity, including coupling and cohesion, cyclomatic complexity, and information hiding ability. A syntactic interface is defined in order to represent all data flow across the module boundary. Four modelling guidelines are also presented to encourage best practice. Also, a custom tool that supports the modelling of Simulink modules is described. Finally, this work is demonstrated and evaluated on a real-world example from the nuclear domain.

Zinovy Diskin, Nicholas Annable, Alan Wassyng et al.

We propose considering assurance as a model management enterprise: saying that a system is safe amounts to specifying three workflows modelling how the safety engineering process is defined and executed, and checking their conformance. These workflows are based on precise data modelling as in functional block diagrams, but their distinctive feature is the presence of relationships between the output data of a process and its input data; hence, the name ``WorkflowPlus'', WF+ . A typical WP^+ model comprises three layers: (i) process and control flow, (ii) dataflow (with input-output relationships), and (iii) argument flow or constraint derivation. Precise dataflow modelling signifies a crucial distinction of (WP+)-based and GSN-based assurance, in which the data layer is mainly implicit. We provide a detailed comparative analysis of the two formalisms and conclude that GSN does not fulfil its promises.

Zinovy Diskin, Harald König, Mark Lawford

Multiple (more than 2) model synchronization is ubiquitous and important for model driven engineering, but its theoretical underpinning gained much less attention than the binary case. Specifically, the latter was extensively studied by the bx community in the framework of algebraic models for update propagation called lenses. Now we make a step to restore the balance and propose a notion of multiary delta lens. Besides multiarity, our lenses feature {\em reflective} updates, when consistency restoration requires some amendment of the update that violated consistency. We emphasize the importance of various ways of lens composition for practical applications of the framework, and prove several composition results.

Linna Pang, Chen-Wei Wang, Mark Lawford et al.

A critical step towards certifying safety-critical systems is to check their conformance to hard real-time requirements. A promising way to achieve this is by building the systems from pre-verified components and verifying their correctness in a compositional manner. We previously reported a formal approach to verifying function blocks (FBs) using tabular expressions and the PVS proof assistant. By applying our approach to the IEC 61131-3 standard of Programmable Logic Controllers (PLCs), we constructed a repository of precise specification and reusable (proven) theorems of feasibility and correctness for FBs. However, we previously did not apply our approach to verify FBs against timing requirements, since IEC 61131-3 does not define composite FBs built from timers. In this paper, based on our experience in the nuclear domain, we conduct two realistic case studies, consisting of the software requirements and the proposed FB implementations for two subsystems of an industrial control system. The implementations are built from IEC 61131-3 FBs, including the on-delay timer. We find issues during the verification process and suggest solutions.