Showing 1–10 of 10 results for author: Lawford, M

Simulation-based Analysis of a Novel Loop-based Road Topology for Autonomous Vehicles

Authors: Stefan Ramdhan, Winnie Trandinh, Sathurshan Arulmohan, Xiayong Hu, Spencer Deevy, Victor Bandur, Vera Pantelic, Mark Lawford, Alan Wassyng

Abstract: The challenges in implementing SAE Level 4/5 autonomous vehicles are manifold, with intersection navigation being a pervasive one. We analyze a novel road topology invented by a co-author of this paper, Xiayong Hu. The topology eliminates the need for traditional traffic control and cross-traffic at intersections, potentially improving the safety of autonomous driving systems. The topology, herein… ▽ More The challenges in implementing SAE Level 4/5 autonomous vehicles are manifold, with intersection navigation being a pervasive one. We analyze a novel road topology invented by a co-author of this paper, Xiayong Hu. The topology eliminates the need for traditional traffic control and cross-traffic at intersections, potentially improving the safety of autonomous driving systems. The topology, herein called the Zonal Road Topology, consists of unidirectional loops of road with traffic flowing either clockwise or counter-clockwise. Adjacent loops are directionally aligned with one another, allowing vehicles to transfer from one loop to another through a simple lane change. To evaluate the Zonal Road Topology, a one km2 pilot-track near Changshu, China is currently being set aside for testing. In parallel, traffic simulations are being performed. To this end, we conduct a simulation-based comparison between the Zonal Road Topology and a traditional road topology for a generic Electric Vehicle (EV) using the Simulation for Urban MObility (SUMO) platform and MATLAB/Simulink. We analyze the topologies in terms of their travel efficiency, safety, energy usage, and capacity. Drive time, number of halts, progress rate, and other metrics are analyzed across varied traffic levels to investigate the advantages and disadvantages of the Zonal Road Topology. Our results indicate that vehicles on the Zonal Road Topology have a lower, more consistent drive time with greater traffic throughput, while using less energy on average. These results become more prominent at higher traffic densities. △ Less

Submitted 2 February, 2024; originally announced February 2024.

Comments: 8 pages, 10 figures, Submitted to IV2024

Test Case Generation for Drivability Requirements of an Automotive Cruise Controller: An Experience with an Industrial Simulator

Authors: Federico Formica, Nicholas Petrunti, Lucas Bruck, Vera Pantelic, Mark Lawford, Claudio Menghi

Abstract: Automotive software development requires engineers to test their systems to detect violations of both functional and drivability requirements. Functional requirements define the functionality of the automotive software. Drivability requirements refer to the driver's perception of the interactions with the vehicle; for example, they typically require limiting the acceleration and jerk perceived by… ▽ More Automotive software development requires engineers to test their systems to detect violations of both functional and drivability requirements. Functional requirements define the functionality of the automotive software. Drivability requirements refer to the driver's perception of the interactions with the vehicle; for example, they typically require limiting the acceleration and jerk perceived by the driver within given thresholds. While functional requirements are extensively considered by the research literature, drivability requirements garner less attention. This industrial paper describes our experience assessing the usefulness of an automated search-based software testing (SBST) framework in generating failure-revealing test cases for functional and drivability requirements. Our experience concerns the VI-CarRealTime simulator, an industrial virtual modeling and simulation environment widely used in the automotive domain. We designed a Cruise Control system in Simulink for a four-wheel vehicle, in an iterative fashion, by producing 21 model versions. We used the SBST framework for each version of the model to search for failure-revealing test cases revealing requirement violations. Our results show that the SBST framework successfully identified a failure-revealing test case for 66.7% of our model versions, requiring, on average, 245.9s and 3.8 iterations. We present lessons learned, reflect on the generality of our results, and discuss how our results improve the state of practice. △ Less

Submitted 29 May, 2023; originally announced May 2023.

Comments: 10 pages papaer plus 2 of bibliography. 10 figures and 6 tables

Novel Fundus Image Preprocessing for Retcam Images to Improve Deep Learning Classification of Retinopathy of Prematurity

Authors: Sajid Rahim, Kourosh Sabri, Anna Ells, Alan Wassyng, Mark Lawford, Linyang Chu, Wenbo He

Abstract: 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 fo… ▽ More 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. △ Less

Submitted 17 June, 2024; v1 submitted 5 February, 2023; originally announced February 2023.

Comments: 10 pages, 4 figures, 7 tables. arXiv admin note: text overlap with arXiv:1904.08796 by other authors

ACM Class: I.2.1

Simulation-based Testing of Simulink Models with Test Sequence and Test Assessment Blocks

Authors: Federico Formica, Tony Fan, Akshay Rajhans, Vera Pantelic, Mark Lawford, Claudio Menghi

Abstract: Simulation-based software testing supports engineers in finding faults in Simulink models. It typically relies on search algorithms that iteratively generate test inputs used to exercise models in simulation to detect design errors. While simulation-based software testing techniques are effective in many practical scenarios, they are typically not fully integrated within the Simulink environment a… ▽ More Simulation-based software testing supports engineers in finding faults in Simulink models. It typically relies on search algorithms that iteratively generate test inputs used to exercise models in simulation to detect design errors. While simulation-based software testing techniques are effective in many practical scenarios, they are typically not fully integrated within the Simulink environment and require additional manual effort. Many techniques require engineers to specify requirements using logical languages that are neither intuitive nor fully supported by Simulink, thereby limiting their adoption in industry. This work presents HECATE, a testing approach for Simulink models using Test Sequence and Test Assessment blocks from Simulink Test. Unlike existing testing techniques, HECATE uses information from Simulink models to guide the search-based exploration. Specifically, HECATE relies on information provided by the Test Sequence and Test Assessment blocks to guide the search procedure. Across a benchmark of 16 Simulink models from different domains and industries, our comparison of HECATE with the state-of-the-art testing tool S-TALIRO indicates that HECATE is both more effective (more failure-revealing test cases) and efficient (less iterations and computational time) than S-TALIRO for ~94% and ~81% of benchmark models respectively. Furthermore, HECATE successfully generated a failure-revealing test case for a representative case study from the automotive domain demonstrating its practical usefulness. △ Less

Submitted 22 December, 2022; originally announced December 2022.

Is the Rush to Machine Learning Jeopardizing Safety? Results of a Survey

Authors: Mehrnoosh Askarpour, Alan Wassyng, Mark Lawford, Richard Paige, Zinovy Diskin

Abstract: 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 introd… ▽ More 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. △ Less

Submitted 28 November, 2021; originally announced November 2021.

Literature Review of Computer Tools for the Visually Impaired: a focus on Search Engines

Authors: Guy Meyer, Alan Wassyng, Mark Lawford, Kourosh Sabri, Shahram Shirani

Abstract: 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… ▽ More 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. △ Less

Submitted 21 October, 2020; originally announced October 2020.

Comments: 103 pages

ACM Class: D.2.2; H.1.2; H.3.3; H.3.5

Supporting Modularity in Simulink Models

Authors: Monika Jaskolka, Vera Pantelic, Alan Wassyng, Mark Lawford

Abstract: 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 text… ▽ More 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. △ Less

Submitted 20 July, 2020; originally announced July 2020.

Assurance via workflow+ modelling and conformance

Authors: Zinovy Diskin, Nicholas Annable, Alan Wassyng, Mark Lawford

Abstract: 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 outp… ▽ More 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. △ Less

Submitted 20 December, 2019; originally announced December 2019.

Multiple Model Synchronization with Multiary Delta Lenses with Amendment and K-Putput

Authors: Zinovy Diskin, Harald König, Mark Lawford

Abstract: 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 multi… ▽ More 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. △ Less

Submitted 25 November, 2019; originally announced November 2019.

Comments: The version published at FAC has multiple essential typos in section 7.1, which make that section practically unreadable

Journal ref: Formal Aspects of Computing 31(5): 611-640 (2019)

Formal Verification of Real-Time Function Blocks Using PVS

Authors: Linna Pang, Chen-Wei Wang, Mark Lawford, Alan Wassyng, Josh Newell, Vera Chow, David Tremaine

Abstract: 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. B… ▽ More 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. △ Less

Submitted 11 June, 2015; originally announced June 2015.

Comments: In Proceedings ESSS 2015, arXiv:1506.03250

ACM Class: D.2.4; F.4.1

Journal ref: EPTCS 184, 2015, pp. 65-79