John Fitzgerald

John Fitzgerald, Tomohiro Oda, Hugo Daniel Macedo

This volume contains the papers presented at the 18th International Overture Workshop, held online on 7th December 2020. This event was the latest in a series of workshops around the Vienna Development Method (VDM), the open-source project Overture, and related tools and formalisms. VDM is one of the longest established formal methods for systems development. A lively community of researchers and practitioners has grown up in academia and industry has grown around the modelling languages (VDM-SL, VDM++, VDM-RT, CML) and tools (VDMTools, Overture, Crescendo, Symphony, the INTO-CPS chain, and ViennaTalk). Together, these provide a platform for work on modelling and analysis technology that includes static and dynamic analysis, test generation, execution support, and model checking. This workshop provided updates on the emerging technology of VDM/Overture, including collaboration infrastructure, collaborative modelling and co-simulation for Cyber-Physical Systems.

Tairan Liu, Kevin de Haan, Bijie Bai et al.

Polarized light microscopy provides high contrast to birefringent specimen and is widely used as a diagnostic tool in pathology. However, polarization microscopy systems typically operate by analyzing images collected from two or more light paths in different states of polarization, which lead to relatively complex optical designs, high system costs or experienced technicians being required. Here, we present a deep learning-based holographic polarization microscope that is capable of obtaining quantitative birefringence retardance and orientation information of specimen from a phase recovered hologram, while only requiring the addition of one polarizer/analyzer pair to an existing holographic imaging system. Using a deep neural network, the reconstructed holographic images from a single state of polarization can be transformed into images equivalent to those captured using a single-shot computational polarized light microscope (SCPLM). Our analysis shows that a trained deep neural network can extract the birefringence information using both the sample specific morphological features as well as the holographic amplitude and phase distribution. To demonstrate the efficacy of this method, we tested it by imaging various birefringent samples including e.g., monosodium urate (MSU) and triamcinolone acetonide (TCA) crystals. Our method achieves similar results to SCPLM both qualitatively and quantitatively, and due to its simpler optical design and significantly larger field-of-view, this method has the potential to expand the access to polarization microscopy and its use for medical diagnosis in resource limited settings.

Peter Gorm Larsen, Hugo Daniel Macedo, John Fitzgerald et al.

Businesses, particularly small and medium-sized enterprises, aiming to start up in Model-Based Design (MBD) face difficult choices from a wide range of methods, notations and tools before making the significant investments in planning, procurement and training necessary to deploy new approaches successfully. In the development of Cyber-Physical Systems (CPSs) this is exacerbated by the diversity of formalisms covering computation, physical and human processes. In this paper, we propose the use of a cloud-enabled and open collaboration platform that allows businesses to offer models, tools and other assets, and permits others to access these on a pay-per-use basis as a means of lowering barriers to the adoption of MBD technology, and to promote experimentation in a sandbox environment.

Oldrich Faldik, Richard Payne, John Fitzgerald et al.

A key challenge in System of Systems (SoS) engineering is the analysis and maintenance of global properties under SoS evolution, and the integration of new constituent elements. There is a need to model the constituent systems composing a SoS in order to allow the analysis of emergent behaviours at the SoS boundary. The Contract pattern allows the engineer to specify constrained behaviours to which constituent systems are required to conform in order to be a part of the SoS. However, the Contract pattern faces some limitations in terms of its accessibility and suitability for verifying contract compatibility. To address these deficiencies, we propose the enrichment of the Contract pattern, which hitherto has been defined using SysML and the COMPASS Modelling Language (CML), by utilising SysML and Object Constraint Language (OCL). In addition, we examine the potential of interface automata, a notation for improving loose coupling between interfaces of constituent systems defined according to the contract, as a means of enabling the verification of contract compatibility. The approach is demonstrated using a case study in audio/video content streaming.

Claire Ingram, Steve Riddle, John Fitzgerald et al.

Systems of systems (SoSs) are particularly vulnerable to faults and other threats to their dependability, but frequently inhabit domains that demand high levels of dependability. For this reason fault tolerance analysis is important in SoS engineering. The COMPASS project has previously proposed a Fault Tolerance Architecture Framework (FMAF), consisting of a collection of viewpoints that support systematic reasoning about faults in an SoS at the architectural level. The FMAF has been demonstrated previously with an analysis of an example fault in an emergency response SoS. In this paper we present further examples of the FMAF's practical use, by analysing different types of faults drawn from the same emergency response case study. These example faults exercise different aspects of the FMAF, demonstrate its use in more complex fault modelling scenarios, and raise new questions for further development.