Towards requirements aware systems:run-time resolution of design-time assumptions

In earlier work we proposed the idea of requirements-aware systems that could introspect about the extent to which their goals were being satisfied at runtime. When combined with requirements monitoring and self adaptive capabilities, requirements awareness should help optimize goal satisfaction even in the presence of changing run-time context. In this paper we describe initial progress towards the realization of requirements-aware systems with REAssuRE. REAssuRE focuses on explicit representation of assumptions made at design time. When such assumptions are shown not to hold, REAssuRE can trigger system adaptations to alternative goal realization strategies.

Optical and structural ocular changes during incipient presbyopia

The primary aim of this thesis was to investigate the in vivo ocular morphological and contractile changes occurring within the accommodative apparatus prior to the onset of presbyopia, with particular reference to ciliary muscle changes with age and the origin of a myopic shift in refraction during incipient presbyopia. Commissioned semi-automated software proved capable of extracting accurate and repeatable measurements from crystalline lens and ciliary muscle Anterior Segment Optical Coherence Tomography (AS-OCT) images and reduced the subjectivity of AS-OCT image analysis. AS-OCT was utilised to document longitudinal changes in ciliary muscle morphology within an incipient presbyopic population (n=51). A significant antero-inwards shift of ciliary muscle mass was observed after 2.5 years. Furthermore, in a subgroup study (n=20), an accommodative antero-inwards movement of ciliary muscle mass was evident. After 2.5 years, the centripetal response of the ciliary muscle significantly attenuated during accommodation, whereas the antero-posterior mobility of the ciliary muscle remained invariant. Additionally, longitudinal measurement of ocular biometry revealed a significant increase in crystalline lens thickness and a corresponding decrease in anterior chamber depth after 2.5 years (n=51). Lenticular changes appear to be determinant of changes in refraction during incipient presbyopia. During accommodation, a significant increase in crystalline lens thickness and axial length was observed, whereas anterior chamber depth decreased (n=20). The change in ocular biometry per dioptre of accommodation exerted remained invariant after 2.5 years. Cross-sectional ocular biometric data were collected to quantify accommodative axial length changes from early adulthood to advanced presbyopia (n=72). Accommodative axial length elongation significantly attenuated during presbyopia, which was consistent with a significant increase in ocular rigidity during presbyopia. The studies presented in this thesis support the Helmholtz theory of accommodation and despite the reduction in centripetal ciliary muscle contractile response with age, primarily implicate lenticular changes in the development of presbyopia.

Reliability of retinal vessel calibre measurements using a retinal oximeter

Background: Summarised retinal vessel diameters are linked to systemic vascular pathology. Monochromatic images provide best contrast to measure vessel calibres. However, when obtaining images with a dual wavelength oximeter the red-free image can be extracted as the green channel information only which in turn will reduce the number of photographs taken at a given time. This will reduce patient exposure to the camera flash and could provide sufficient quality images to reliably measure vessel calibres. Methods: We obtained retinal images of one eye of 45 healthy participants. Central retinal arteriolar and central retinal venular equivalents (CRAE and CRVE, respectively) were measured using semi-automated software from two monochromatic images: one taken with a red-free filter and one extracted from the green channel of a dual wavelength oximetry image. Results: Participants were aged between 21 and 62 years, all were normotensive (SBP: 115 (12) mmHg; DBP: 72 (10) mmHg) and had normal intra-ocular pressures (12 (3) mmHg). Bland-Altman analysis revealed good agreement of CRAE and CRVE as obtained from both images (mean bias CRAE = 0.88; CRVE = 2.82). Conclusions: Summarised retinal vessel calibre measurements obtained from oximetry images are in good agreement to those obtained using red-free photographs.

An automated tool for semantic accessing to formal software models

Many software engineers have found that it is difficult to understand, incorporate and use different formal models consistently in the process of software developments, especially for large and complex software systems. This is mainly due to the complex mathematical nature of the formal methods and the lack of tool support. It is highly desirable to have software models and their related software artefacts systematically connected and used collaboratively, rather than in isolation. The success of the Semantic Web, as the next generation of Web technology, can have profound impact on the environment for formal software development. It allows both the software engineers and machines to understand the content of formal models and supports more effective software design in terms of understanding, sharing and reusing in a distributed manner. To realise the full potential of the Semantic Web in formal software development, effectively creating proper semantic metadata for formal software models and their related software artefacts is crucial. This paper proposed a framework that allows users to interconnect the knowledge about formal software models and other related documents using the semantic technology. We first propose a methodology with tool support is proposed to automatically derive ontological metadata from formal software models and semantically describe them. We then develop a Semantic Web environment for representing and sharing formal Z/OZ models. A method with prototype tool is presented to enhance semantic query to software models and other artefacts. © 2014.

Software engineering techniques for the development of systems of systems

This paper investigates how existing software engineering techniques can be employed, adapted and integrated for the development of systems of systems. Starting from existing system-of-systems (SoS) studies, we identify computing paradigms and techniques that have the potential to help address the challenges associated with SoS development, and propose an SoS development framework that combines these techniques in a novel way. This framework addresses the development of a class of IT systems of systems characterised by high variability in the types of interactions between their component systems, and by relatively small numbers of such interactions. We describe how the framework supports the dynamic, automated generation of the system interfaces required to achieve these interactions, and present a case study illustrating the development of a data-centre SoS using the new framework.

Managing performance of organisational units with PIMsoft:a new DEA software

DEA literature continues apace but software has lagged behind. This session uses suitably selected data to present newly developed software which includes many of the most recent DEA models. The software enables the user to address a variety of issues not frequently found in existing DEA software such as: -Assessments under a variety of possible assumptions of returns to scale including NIRS and NDRS; -Scale elasticity computations; -Numerous Input/Output variables and truly unlimited number of assessment units (DMUs) -Panel data analysis -Analysis of categorical data (multiple categories) -Malmquist Index and its decompositions -Computations of Supper efficiency -Automated removal of super-efficient outliers under user-specified criteria; -Graphical presentation of results -Integrated statistical tests

Polynomial function intervals for floating-point software verification

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs. © 2014 Springer International Publishing Switzerland.

Design software architecture models using ontology

Software architecture plays an essential role in the high level description of a system design, where the structure and communication are emphasized. Despite its importance in the software engineering process, the lack of formal description and automated verification hinders the development of good software architecture models. In this paper, we present an approach to support the rigorous design and verification of software architecture models using the semantic web technology. We view software architecture models as ontology representations, where their structures and communication constraints are captured by the Web Ontology Language (OWL) and the Semantic Web Rule Language (SWRL). Specific configurations on the design are represented as concrete instances of the ontology, to which their structures and dynamic behaviors must conform. Furthermore, ontology reasoning tools can be applied to perform various automated verification on the design to ensure correctness, such as consistency checking, style recognition, and behavioral inference.