-
Translating a VDM Model of a Medical Device into Kapture
Authors:
Joe Hare,
Leo Freitas,
Ken Pierce
Abstract:
As the complexity of safety-critical medical devices increases, so does the need for clear, verifiable, software requirements. This paper explores the use of Kapture, a formal modelling tool developed by D-RisQ, to translate an existing formal VDM model of a medical implant for treating focal epilepsy called CANDO. The work was undertaken without prior experience in formal methods. The paper asses…
▽ More
As the complexity of safety-critical medical devices increases, so does the need for clear, verifiable, software requirements. This paper explores the use of Kapture, a formal modelling tool developed by D-RisQ, to translate an existing formal VDM model of a medical implant for treating focal epilepsy called CANDO. The work was undertaken without prior experience in formal methods. The paper assess Kapture's usability, the challenges of formal modelling, and the effectiveness of the translated model. The result is a model in Kapture which covers over 90% of the original VDM model, and produces matching traces of results. While several issues were encountered during design and implementation, mainly due to the initial learning curve, this paper demonstrates that complex systems can be effectively modelled in Kapture by inexperienced users and highlights some difficulties in translating VDM specifications to Kapture.
△ Less
Submitted 11 June, 2025;
originally announced June 2025.
-
Proceedings of the 23rd International Overture Workshop
Authors:
Hugo Daniel Macedo,
Ken Pierce
Abstract:
This volume contains the papers presented at the 23rd International Overture Workshop, held on the 11th of June 2025. 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 pra…
▽ More
This volume contains the papers presented at the 23rd International Overture Workshop, held on the 11th of June 2025. 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.
△ Less
Submitted 10 June, 2025;
originally announced June 2025.
-
Proceedings of the 22nd International Overture Workshop
Authors:
Hugo Daniel Macedo,
Ken Pierce,
Leo Freitas
Abstract:
This volume contains the papers presented at the 22nd International Overture Workshop, held on the 10th of September 2024. 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 an…
▽ More
This volume contains the papers presented at the 22nd International Overture Workshop, held on the 10th of September 2024. 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.
△ Less
Submitted 30 September, 2024;
originally announced October 2024.
-
Proceedings of the 21st International Overture Workshop
Authors:
Hugo Daniel Macedo,
Ken Pierce
Abstract:
This volume contains the papers presented at the 21st International Overture Workshop, held on the 10th of March 2023. 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 pr…
▽ More
This volume contains the papers presented at the 21st International Overture Workshop, held on the 10th of March 2023. 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.
△ Less
Submitted 17 November, 2023; v1 submitted 13 November, 2023;
originally announced November 2023.
-
Modelling Maritime SAR Effective Sweep Widths for Helicopters in VDM
Authors:
Alexander Sulaiman,
Ken Pierce
Abstract:
Search and Rescue (SAR) is searching for and providing help to people in danger. In the UK, SAR teams are typically charities with limited resources, and SAR missions are time critical. Search managers need to objectively decide which search assets (e.g. helicopter vs drone) would be better. A key metric in the SAR community is effective sweep width (W), which provides a single measure for a searc…
▽ More
Search and Rescue (SAR) is searching for and providing help to people in danger. In the UK, SAR teams are typically charities with limited resources, and SAR missions are time critical. Search managers need to objectively decide which search assets (e.g. helicopter vs drone) would be better. A key metric in the SAR community is effective sweep width (W), which provides a single measure for a search asset's ability to detect a specific object in specific environmental conditions. Tables of W for different search assets are provided in various manuals, such as the International Aeronautical and Maritime SAR (IAMSAR) Manual. However, these tables take years of expensive testing and experience to produce, and no such tables exist for drones. This paper uses the Vienna Development Method (VDM) to build an initial model of W for a known case (helicopters at sea) with a view to predicting W tables for drones. The model computes W for various search object sizes, helicopter altitude and visibility. The results for the model are quite different from the published tables, which shows that the abstraction level is not yet correct, however it produced useful insights and directions for the next steps.
△ Less
Submitted 29 March, 2023;
originally announced April 2023.
-
Proceedings of the 20th International Overture Workshop
Authors:
Hugo Daniel Macedo,
Ken Pierce
Abstract:
This volume contains the papers presented at the 20th International Overture Workshop, which was held in an hybrid format: online and physically at Aarhus, Denmark on 05th July 2022. 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 f…
▽ More
This volume contains the papers presented at the 20th International Overture Workshop, which was held in an hybrid format: online and physically at Aarhus, Denmark on 05th July 2022. 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 around the modelling languages (VDM-SL, VDM++, VDM-RT, CML) and tools (VDMTools, Overture, VDM VSCode extension, 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.
△ Less
Submitted 22 August, 2022;
originally announced August 2022.
-
Recognition and Co-Analysis of Pedestrian Activities in Different Parts of Road using Traffic Camera Video
Authors:
Weijia Xu,
Heidi Ross,
Joel Meyer,
Kelly Pierce,
Natalia Ruiz Juri,
Jennifer Duthie
Abstract:
Pedestrian safety is a priority for transportation system managers and operators, and a main focus of the Vision Zero strategy employed by the City of Austin, Texas. While there are a number of treatments and technologies to effectively improve pedestrian safety, identifying the location where these treatments are most needed remains a challenge. Current practice requires manual observation of can…
▽ More
Pedestrian safety is a priority for transportation system managers and operators, and a main focus of the Vision Zero strategy employed by the City of Austin, Texas. While there are a number of treatments and technologies to effectively improve pedestrian safety, identifying the location where these treatments are most needed remains a challenge. Current practice requires manual observation of candidate locations for limited time periods, leading to an identification process that is time consuming, lags behind traffic pattern changes over time, and lacks scalability. Mid-block locations, where safety countermeasures are often needed the most, are especially hard to identify and monitor. The goal for this research is to understand the correlation between bus stop locations and mid-block crossings, so as to assist traffic engineers in implementing Vision Zero strategies to improve pedestrian safety. In a prior work, we have developed a tool to detect pedestrian crossing events with traffic camera video using a deep neural network model to identify crossing events. In this paper, we extend the methods to identify bus stop usage with traffic camera video from off-the-shelf CCTV pan-tilt-zoom (PTZ) traffic monitoring cameras installed at nearby intersections. We correlate the video detection results for mid-block crossings near a bus stop, with pedestrian activity at the bus stops in each side of the mid-block crossing. We also implement a web portal to facilitate manual review of pedestrian activity detections by automating creation of video clips that show only crossing events, thereby vastly improving the efficiency of the human review process.
△ Less
Submitted 27 November, 2021;
originally announced November 2021.
-
Proceedings of the 19th International Overture Workshop
Authors:
Hugo Daniel Macedo,
Casper Thule,
Ken Pierce
Abstract:
This volume contains the papers presented at the 19th International Overture Workshop, which was held in an hybrid format: online and physically at Aarhus, Denmark on 22th October 2021. 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 method…
▽ More
This volume contains the papers presented at the 19th International Overture Workshop, which was held in an hybrid format: online and physically at Aarhus, Denmark on 22th October 2021. 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 around the modelling languages (VDM-SL, VDM++, VDM-RT, CML) and tools (VDMTools, Overture, VDM VSCode extension, 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.
△ Less
Submitted 18 October, 2021;
originally announced October 2021.
-
An Empirical Comparison of Formalisms for Modelling and Analysis of Dynamic Reconfiguration of Dependable Systems
Authors:
Anirban Bhattacharyya,
Andrey Mokhov,
Ken Pierce
Abstract:
This paper uses a case study to evaluate empirically three formalisms of different kinds for their suitability for the modelling and analysis of dynamic reconfiguration of dependable systems. The requirements on an ideal formalism for dynamic software reconfiguration are defined. The reconfiguration of an office workflow for order processing is described, and the requirements on the reconfiguratio…
▽ More
This paper uses a case study to evaluate empirically three formalisms of different kinds for their suitability for the modelling and analysis of dynamic reconfiguration of dependable systems. The requirements on an ideal formalism for dynamic software reconfiguration are defined. The reconfiguration of an office workflow for order processing is described, and the requirements on the reconfiguration of the workflow are defined. The workflow is modelled using the Vienna Development Method ($\mathrm{VDM}$), conditional partial order graphs ($\mathrm{CPOGs}$), and the basic Calculus of Communicating Systems for dynamic process reconfiguration (basic $\mathrm{CCS^{dp}}$), and verification of the reconfiguration requirements is attempted using the models. The formalisms are evaluated according to their ability to model the reconfiguration of the workflow, to verify the requirements on the workflow's reconfiguration, and to meet the requirements on an ideal formalism.
△ Less
Submitted 27 September, 2016;
originally announced September 2016.
-
On Formalisms for Dynamic Reconfiguration of Dependable Systems
Authors:
Anirban Bhattacharyya,
Andrey Mokhov,
Ken Pierce,
Manuel Mazzara
Abstract:
Three formalisms of different kinds - VDM, Maude, and basic CCSdp - are evaluated for their suitability for the modelling and verification of dynamic software reconfiguration using as a case study the dynamic reconfiguration of a simple office workflow for order processing. The research is ongoing, and initial results are reported.
Three formalisms of different kinds - VDM, Maude, and basic CCSdp - are evaluated for their suitability for the modelling and verification of dynamic software reconfiguration using as a case study the dynamic reconfiguration of a simple office workflow for order processing. The research is ongoing, and initial results are reported.
△ Less
Submitted 7 May, 2014; v1 submitted 1 May, 2014;
originally announced May 2014.
