Showing 1–24 of 24 results for author: Butler, M

Design Considerations for Automatic Musical Soundscapes of Visual Art for People with Blindness or Low Vision

Authors: Stephen James Krol, Maria Teresa Llano, Matthew Butler, Cagatay Goncu

Abstract: Music has been identified as a promising medium to enhance the accessibility and experience of visual art for people who are blind or have low vision (BLV). However, composing music and designing soundscapes for visual art is a time-consuming, resource intensive process - limiting its scalability for large exhibitions. In this paper, we investigate the use of automated soundscapes to increase the… ▽ More Music has been identified as a promising medium to enhance the accessibility and experience of visual art for people who are blind or have low vision (BLV). However, composing music and designing soundscapes for visual art is a time-consuming, resource intensive process - limiting its scalability for large exhibitions. In this paper, we investigate the use of automated soundscapes to increase the accessibility of visual art. We built a prototype system and ran a qualitative study to evaluate the aesthetic experience provided by the automated soundscapes with 10 BLV participants. From the study, we identified a set of design considerations that reveal requirements from BLV people for the development of automated soundscape systems, setting new directions in which creative systems could enrich the aesthetic experience conveyed by these. △ Less

Submitted 23 May, 2024; originally announced May 2024.

Comments: Paper accepted into ICCC 24

An AIC-based approach for articulating unpredictable problems in open complex environments

Authors: Haider AL-Shareefy, Michael Butler, Thai Son Hoang

Abstract: This research paper presents an approach to enhancing the predictive capability of architects in the design and assurance of systems, focusing on systems operating in dynamic and unpredictable environments. By adopting a systems approach, we aim to improve architects' predictive capabilities in designing dependable systems (for example, ML-based systems). An aerospace case study is used to illustr… ▽ More This research paper presents an approach to enhancing the predictive capability of architects in the design and assurance of systems, focusing on systems operating in dynamic and unpredictable environments. By adopting a systems approach, we aim to improve architects' predictive capabilities in designing dependable systems (for example, ML-based systems). An aerospace case study is used to illustrate the approach. Multiple factors (challenges) influencing aircraft detection are identified, demonstrating the effectiveness of our approach in a complex operational setting. Our approach primarily aimed to enhance the architect's predictive capability. △ Less

Submitted 15 March, 2024; originally announced March 2024.

Comments: S. Bernardi, T. Zoppi (Editors), "Fast Abstracts and Student Forum Proceedings - EDCC 2024 - 19th European Dependable Computing Conference, Leuven, Belgium, 8-11 April 2024"

Refreshable Tactile Displays for Accessible Data Visualisation

Authors: Leona Holloway, Peter Cracknell, Kate Stephens, Melissa Fanshawe, Samuel Reinders, Kim Marriott, Matthew Butler

Abstract: Refreshable tactile displays (RTDs) are predicted to soon become a viable option for the provision of accessible graphics for people who are blind or have low vision (BLV). This new technology for the tactile display of braille and graphics, usually using raised pins, makes it easier to generate and access a large number of graphics. However, it differs from existing tactile graphics in terms of s… ▽ More Refreshable tactile displays (RTDs) are predicted to soon become a viable option for the provision of accessible graphics for people who are blind or have low vision (BLV). This new technology for the tactile display of braille and graphics, usually using raised pins, makes it easier to generate and access a large number of graphics. However, it differs from existing tactile graphics in terms of scale, height and fidelity. Here, we share the perspectives of four key stakeholders -- blind touch readers, vision specialist teachers, accessible format producers and assistive technology providers -- to explore the potential uses, advantages and needs relating to the introduction of RTDs. We also provide advice on what role the data visualisation community can take to help ensure that people who are BLV are best able to benefit from the introduction of affordable RTDs. △ Less

Submitted 28 January, 2024; originally announced January 2024.

Comments: Poster presented at IEEE VIS 2023 (Best Poster Honorable Mentions)

Designing Conversational Multimodal 3D Printed Models with People who are Blind

Authors: Samuel Reinders, Swamy Ananthanarayan, Matthew Butler, Kim Marriott

Abstract: 3D printed models have been used to improve access to graphical information by people who are blind, offering benefits over conventional accessible graphics. Here we investigate an interactive 3D printed model (I3M) that combines a conversational interface with haptic vibration and touch to provide more natural and accessible experiences. Specifically, we co-designed a multimodal model of the Sola… ▽ More 3D printed models have been used to improve access to graphical information by people who are blind, offering benefits over conventional accessible graphics. Here we investigate an interactive 3D printed model (I3M) that combines a conversational interface with haptic vibration and touch to provide more natural and accessible experiences. Specifically, we co-designed a multimodal model of the Solar System with nine blind people and evaluated the prototype with another seven blind participants. We discuss our journey from a design perspective, focusing on touch, conversational and multimodal interactions. Based on our experience, we suggest design recommendations that consider blind users' desire for independence and control, customisation, comfort and use of prior experience △ Less

Submitted 11 June, 2023; originally announced June 2023.

Comments: To appear in ACM Designing Interactive Systems Conference (DIS '23), July 10-14, 2023, Pittsburgh, PA, USA

Digital Resilience and the Continuance Use of Mobile Payment Services

Authors: Muftawu Dzang Alhassan, Martin Butler

Abstract: The use of mobile payment services is an essential contributor to financial inclusion in emerging markets. Unfortunately, the service has become a platform for fraud. Mobile payment users need to be digitally resilient to continue using the service after adverse events. However, there is scant literature on users' continuance use of mobile payment services in the post-event of fraud. The focal poi… ▽ More The use of mobile payment services is an essential contributor to financial inclusion in emerging markets. Unfortunately, the service has become a platform for fraud. Mobile payment users need to be digitally resilient to continue using the service after adverse events. However, there is scant literature on users' continuance use of mobile payment services in the post-event of fraud. The focal point of prior literature has been on technology adoption or threat avoidance to implement policies that protect users. Analysing the relationship between individual digital resilience and post-adoption behavioural patterns will enable service providers to support individual digital resilience to promote users' continuance use of the service. This research aims to develop and empirically validate a conceptual model to examine individual digital resilience in the context of the continuance use of mobile payments. The model will be based on protection motivation theory. Survey data will be obtained from victims of mobile payment fraud and other users who continue using the service despite their knowledge of mobile payment fraud. The results from this study are expected to make key contributions to theory, practice, and policy in the areas of digital resilience, mobile payments, and ICT4D. △ Less

Submitted 22 August, 2021; originally announced August 2021.

Comments: In proceedings of the 1st Virtual Conference on Implications of Information and Digital Technologies for Development, 2021

Technology Developments in Touch-Based Accessible Graphics: A Systematic Review of Research 2010-2020

Authors: Matthew Butler, Leona Holloway, Samuel Reinders, Cagatay Goncu, Kim Marriott

Abstract: This paper presents a systematic literature review of 292 publications from 97 unique venues on touch-based graphics for people who are blind or have low vision, from 2010 to mid-2020. It is the first review of its kind on touch-based accessible graphics. It is timely because it allows us to assess the impact of new technologies such as commodity 3D printing and low-cost electronics on the product… ▽ More This paper presents a systematic literature review of 292 publications from 97 unique venues on touch-based graphics for people who are blind or have low vision, from 2010 to mid-2020. It is the first review of its kind on touch-based accessible graphics. It is timely because it allows us to assess the impact of new technologies such as commodity 3D printing and low-cost electronics on the production and presentation of accessible graphics. As expected our review shows an increase in publications from 2014 that we can attribute to these developments. It also reveals the need to: broaden application areas, especially to the workplace; broaden end-user participation throughout the full design process; and conduct more in situ evaluation. This work is linked to an online living resource to be shared with the wider community. △ Less

Submitted 1 February, 2021; originally announced February 2021.

Comments: To appear in ACM CHI Conference on Human Factors in Computing Systems (CHI '21), May 8-13, 2021, Yokohama, Japan

SeqGenSQL -- A Robust Sequence Generation Model for Structured Query Language

Authors: Ning Li, Bethany Keller, Mark Butler, Daniel Cer

Abstract: We explore using T5 (Raffel et al. (2019)) to directly translate natural language questions into SQL statements. General purpose natural language that interfaces to information stored within databases requires flexibly translating natural language questions into database queries. The best performing text-to-SQL systems approach this task by first converting questions into an intermediate logical f… ▽ More We explore using T5 (Raffel et al. (2019)) to directly translate natural language questions into SQL statements. General purpose natural language that interfaces to information stored within databases requires flexibly translating natural language questions into database queries. The best performing text-to-SQL systems approach this task by first converting questions into an intermediate logical form (LF) (Lyu et al. (2020)). While LFs provide a convenient intermediate representation and simplify query generation, they introduce an additional layer of complexity and annotation requirements. However, weakly supervised modeling that directly converts questions to SQL statements has proven more difficult without the scaffolding provided by LFs (Min et al. (2019)). We approach direct conversion of questions to SQL statements using T5 (Raffel et al. (2019)), a pre-trained textto-text generation model, modified to support pointer-generator style decoding (See et al. (2017)). We explore using question augmentation with table schema information and the use of automatically generated silver training data. The resulting model achieves 90.5% execution accuracy on the WikiSQL (Zhong et al. (2017)) test data set, a new state-of-the-art on weakly supervised SQL generation. The performance improvement is 6.6% absolute over the prior state-of-the-art (Min et al. (2019)) and approaches the performance of state-ofthe-art systems making use of LFs. △ Less

Submitted 7 November, 2020; originally announced November 2020.

Comments: 6 pages, 7 figures, 2 tables

Model-Based Machine Learning for Joint Digital Backpropagation and PMD Compensation

Authors: Rick M. Bütler, Christian Häger, Henry D. Pfister, Gabriele Liga, Alex Alvarado

Abstract: In this paper, we propose a model-based machine-learning approach for dual-polarization systems by parameterizing the split-step Fourier method for the Manakov-PMD equation. The resulting method combines hardware-friendly time-domain nonlinearity mitigation via the recently proposed learned digital backpropagation (LDBP) with distributed compensation of polarization-mode dispersion (PMD). We refer… ▽ More In this paper, we propose a model-based machine-learning approach for dual-polarization systems by parameterizing the split-step Fourier method for the Manakov-PMD equation. The resulting method combines hardware-friendly time-domain nonlinearity mitigation via the recently proposed learned digital backpropagation (LDBP) with distributed compensation of polarization-mode dispersion (PMD). We refer to the resulting approach as LDBP-PMD. We train LDBP-PMD on multiple PMD realizations and show that it converges within 1% of its peak dB performance after 428 training iterations on average, yielding a peak effective signal-to-noise ratio of only 0.30 dB below the PMD-free case. Similar to state-of-the-art lumped PMD compensation algorithms in practical systems, our approach does not assume any knowledge about the particular PMD realization along the link, nor any knowledge about the total accumulated PMD. This is a significant improvement compared to prior work on distributed PMD compensation, where knowledge about the accumulated PMD is typically assumed. We also compare different parameterization choices in terms of performance, complexity, and convergence behavior. Lastly, we demonstrate that the learned models can be successfully retrained after an abrupt change of the PMD realization along the fiber. △ Less

Submitted 23 October, 2020; originally announced October 2020.

Comments: 10 pages, 11 figures, to appear in the IEEE/OSA Journal of Lightwave Technology

"Hey Model!" - Natural User Interactions and Agency in Accessible Interactive 3D Models

Authors: Samuel Reinders, Matthew Butler, Kim Marriott

Abstract: While developments in 3D printing have opened up opportunities for improved access to graphical information for people who are blind or have low vision (BLV), they can provide only limited detailed and contextual information. Interactive 3D printed models (I3Ms) that provide audio labels and/or a conversational agent interface potentially overcome this limitation. We conducted a Wizard-of-Oz explo… ▽ More While developments in 3D printing have opened up opportunities for improved access to graphical information for people who are blind or have low vision (BLV), they can provide only limited detailed and contextual information. Interactive 3D printed models (I3Ms) that provide audio labels and/or a conversational agent interface potentially overcome this limitation. We conducted a Wizard-of-Oz exploratory study to uncover the multi-modal interaction techniques that BLV people would like to use when exploring I3Ms, and investigated their attitudes towards different levels of model agency. These findings informed the creation of an I3M prototype of the solar system. A second user study with this model revealed a hierarchy of interaction, with BLV users preferring tactile exploration, followed by touch gestures to trigger audio labels, and then natural language to fill in knowledge gaps and confirm understanding. △ Less

Submitted 29 January, 2024; v1 submitted 1 September, 2020; originally announced September 2020.

Comments: Paper presented at ACM CHI 2020: Proceedings of the 2020 CHI Conference on Human Factors in Computing Systems, ACM, New York, April 2020; Replacement: typos corrected, character encoding

Tactile Presentation of Network Data: Text, Matrix or Diagram?

Authors: Yalong Yang, Kim Marriott, Matthew Butler, Cagatay Goncu, Leona Holloway

Abstract: Visualisations are commonly used to understand social, biological and other kinds of networks. Currently, we do not know how to effectively present network data to people who are blind or have low-vision (BLV). We ran a controlled study with 8 BLV participants comparing four tactile representations: organic node-link diagram, grid node-link diagram, adjacency matrix and braille list. We found that… ▽ More Visualisations are commonly used to understand social, biological and other kinds of networks. Currently, we do not know how to effectively present network data to people who are blind or have low-vision (BLV). We ran a controlled study with 8 BLV participants comparing four tactile representations: organic node-link diagram, grid node-link diagram, adjacency matrix and braille list. We found that the node-link representations were preferred and more effective for path following and cluster identification while the matrix and list were better for adjacency tasks. This is broadly in line with findings for the corresponding visual representations. △ Less

Submitted 31 March, 2020; originally announced March 2020.

Comments: To appear in the ACM CHI Conference on Human Factors in Computing Systems (CHI 2020)

Model-Based Machine Learning for Joint Digital Backpropagation and PMD Compensation

Authors: Christian Häger, Henry D. Pfister, Rick M. Bütler, Gabriele Liga, Alex Alvarado

Abstract: We propose a model-based machine-learning approach for polarization-multiplexed systems by parameterizing the split-step method for the Manakov-PMD equation. This approach performs hardware-friendly DBP and distributed PMD compensation with performance close to the PMD-free case. We propose a model-based machine-learning approach for polarization-multiplexed systems by parameterizing the split-step method for the Manakov-PMD equation. This approach performs hardware-friendly DBP and distributed PMD compensation with performance close to the PMD-free case. △ Less

Submitted 25 January, 2020; originally announced January 2020.

Comments: 3 pages, 2 figures

Revisiting Multi-Step Nonlinearity Compensation with Machine Learning

Authors: Christian Häger, Henry D. Pfister, Rick M. Bütler, Gabriele Liga, Alex Alvarado

Abstract: For the efficient compensation of fiber nonlinearity, one of the guiding principles appears to be: fewer steps are better and more efficient. We challenge this assumption and show that carefully designed multi-step approaches can lead to better performance-complexity trade-offs than their few-step counterparts. For the efficient compensation of fiber nonlinearity, one of the guiding principles appears to be: fewer steps are better and more efficient. We challenge this assumption and show that carefully designed multi-step approaches can lead to better performance-complexity trade-offs than their few-step counterparts. △ Less

Submitted 22 April, 2019; originally announced April 2019.

Comments: 4 pages, 3 figures, This is a preprint of a paper submitted to the 2019 European Conference on Optical Communication

DeepSaucer: Unified Environment for Verifying Deep Neural Networks

Authors: Naoto Sato, Hironobu Kuruma, Masanori Kaneko, Yuichiroh Nakagawa, Hideto Ogawa, Thai Son Hoang, Michael Butler

Abstract: In recent years, a number of methods for verifying DNNs have been developed. Because the approaches of the methods differ and have their own limitations, we think that a number of verification methods should be applied to a developed DNN. To apply a number of methods to the DNN, it is necessary to translate either the implementation of the DNN or the verification method so that one runs in the sam… ▽ More In recent years, a number of methods for verifying DNNs have been developed. Because the approaches of the methods differ and have their own limitations, we think that a number of verification methods should be applied to a developed DNN. To apply a number of methods to the DNN, it is necessary to translate either the implementation of the DNN or the verification method so that one runs in the same environment as the other. Since those translations are time-consuming, a utility tool, named DeepSaucer, which helps to retain and reuse implementations of DNNs, verification methods, and their environments, is proposed. In DeepSaucer, code snippets of loading DNNs, running verification methods, and creating their environments are retained and reused as software assets in order to reduce cost of verifying DNNs. The feasibility of DeepSaucer is confirmed by implementing it on the basis of Anaconda, which provides virtual environment for loading a DNN and running a verification method. In addition, the effectiveness of DeepSaucer is demonstrated by usecase examples. △ Less

Submitted 8 November, 2018; originally announced November 2018.

Monte Carlo Methods for the Game Kingdomino

Authors: Magnus Gedda, Mikael Z. Lagerkvist, Martin Butler

Abstract: Kingdomino is introduced as an interesting game for studying game playing: the game is multiplayer (4 independent players per game); it has a limited game depth (13 moves per player); and it has limited but not insignificant interaction among players. Several strategies based on locally greedy players, Monte Carlo Evaluation (MCE), and Monte Carlo Tree Search (MCTS) are presented with variants.… ▽ More Kingdomino is introduced as an interesting game for studying game playing: the game is multiplayer (4 independent players per game); it has a limited game depth (13 moves per player); and it has limited but not insignificant interaction among players. Several strategies based on locally greedy players, Monte Carlo Evaluation (MCE), and Monte Carlo Tree Search (MCTS) are presented with variants. We examine a variation of UCT called progressive win bias and a playout policy (Player-greedy) focused on selecting good moves for the player. A thorough evaluation is done showing how the strategies perform and how to choose parameters given specific time constraints. The evaluation shows that surprisingly MCE is stronger than MCTS for a game like Kingdomino. All experiments use a cloud-native design, with a game server in a Docker container, and agents communicating using a REST-style JSON protocol. This enables a multi-language approach to separating the game state, the strategy implementations, and the coordination layer. △ Less

Submitted 15 July, 2018; v1 submitted 12 July, 2018; originally announced July 2018.

Comments: To be published in IEEE Conference on Computational Intelligence and Games 2018 (IEEE CIG 2018)

Incremental Database Design using UML-B and Event-B

Authors: Ahmed Al-Brashdi, Michael Butler, Abdolbaghi Rezazadeh

Abstract: Correct operation of many critical systems is dependent on the data consistency and integrity properties of underlying databases. Therefore, a verifiable and rigorous database design process is highly desirable. This research aims to investigate and deliver a comprehensive and practical approach for modelling databases in formal methods through layered refinements. The methodology is being guided… ▽ More Correct operation of many critical systems is dependent on the data consistency and integrity properties of underlying databases. Therefore, a verifiable and rigorous database design process is highly desirable. This research aims to investigate and deliver a comprehensive and practical approach for modelling databases in formal methods through layered refinements. The methodology is being guided by a number of case studies, using abstraction and refinement in UML-B and verification with the Rodin tool. UML-B is a graphical representation of the Event-B formalism and the Rodin tool supports verification for Event-B and UML-B. Our method guides developers to model relational databases in UML-B through layered refinement and to specify the necessary constraints and operations on the database. △ Less

Submitted 14 May, 2018; originally announced May 2018.

Comments: In Proceedings IMPEX 2017 and FM&MDD 2017, arXiv:1805.04636

ACM Class: D.2 SOFTWARE ENGINEERING; F.3 LOGICS AND MEANINGS OF PROGRAMS

Journal ref: EPTCS 271, 2018, pp. 34-47

Theory Plug-in for Rodin 3.x

Authors: T. S. Hoang, L. Voisin, A. Salehi, M. Butler, T. Wilkinson, N. Beauger

Abstract: The Theory plug-in enables modellers to extend the mathematical modelling notation for Event-B, with accompanying support for reasoning about the extended language. Previous version of the Theory plug-in has been implemented based on Rodin 2.x. This presentation outline the main improvements to the The- ory plug-in, to be compatible with Rodin 3.x, in terms of both reliability and us- ability. We… ▽ More The Theory plug-in enables modellers to extend the mathematical modelling notation for Event-B, with accompanying support for reasoning about the extended language. Previous version of the Theory plug-in has been implemented based on Rodin 2.x. This presentation outline the main improvements to the The- ory plug-in, to be compatible with Rodin 3.x, in terms of both reliability and us- ability. We will also present the changes that were needed in the Rodin core to accommodate the Theory plug-in. Finally, we identify future enhancements and research directions for the Theory plug-in. △ Less

Submitted 4 January, 2017; originally announced January 2017.

Comments: Event-B day 2016, Tokyo

ACM Class: D.2.4

Neural Discourse Modeling of Conversations

Authors: John M. Pierre, Mark Butler, Jacob Portnoff, Luis Aguilar

Abstract: Deep neural networks have shown recent promise in many language-related tasks such as the modeling of conversations. We extend RNN-based sequence to sequence models to capture the long range discourse across many turns of conversation. We perform a sensitivity analysis on how much additional context affects performance, and provide quantitative and qualitative evidence that these models are able t… ▽ More Deep neural networks have shown recent promise in many language-related tasks such as the modeling of conversations. We extend RNN-based sequence to sequence models to capture the long range discourse across many turns of conversation. We perform a sensitivity analysis on how much additional context affects performance, and provide quantitative and qualitative evidence that these models are able to capture discourse relationships across multiple utterances. Our results quantifies how adding an additional RNN layer for modeling discourse improves the quality of output utterances and providing more of the previous conversation as input also improves performance. By searching the generated outputs for specific discourse markers we show how neural discourse models can exhibit increased coherence and cohesion in conversations. △ Less

Submitted 15 July, 2016; originally announced July 2016.

Formal Modelling, Testing and Verification of HSA Memory Models using Event-B

Authors: Ashish Darbari, Iain Singleton, Michael Butler, John Colley

Abstract: The HSA Foundation has produced the HSA Platform System Architecture Specification that goes a long way towards addressing the need for a clear and consistent method for specifying weakly consistent memory. HSA is specified in a natural language which makes it open to multiple ambiguous interpretations and could render bugs in implementations of it in hardware and software. In this paper we presen… ▽ More The HSA Foundation has produced the HSA Platform System Architecture Specification that goes a long way towards addressing the need for a clear and consistent method for specifying weakly consistent memory. HSA is specified in a natural language which makes it open to multiple ambiguous interpretations and could render bugs in implementations of it in hardware and software. In this paper we present a formal model of HSA which can be used in the development and verification of both concurrent software applications as well as in the development and verification of the HSA-compliant platform itself. We use the Event-B language to build a provably correct hierarchy of models from the most abstract to a detailed refinement of HSA close to implementation level. Our memory models are general in that they represent an arbitrary number of masters, programs and instruction interleavings. We reason about such general models using refinements. Using Rodin tool we are able to model and verify an entire hierarchy of models using proofs to establish that each refinement is correct. We define an automated validation method that allows us to test baseline compliance of the model against a suite of published HSA litmus tests. Once we complete model validation we develop a coverage driven method to extract a richer set of tests from the Event-B model and a user specified coverage model. These tests are used for extensive regression testing of hardware and software systems. Our method of refinement based formal modelling, baseline compliance testing of the model and coverage driven test extraction using the single language of Event-B is a new way to address a key challenge facing the design and verification of multi-core systems. △ Less

Submitted 16 May, 2016; originally announced May 2016.

Comments: 9 pages, 10 figures

Modelling and Refinement in CODA

Authors: Michael Butler, John Colley, Andrew Edmunds, Colin Snook, Neil Evans, Neil Grant, Helen Marshall

Abstract: This paper provides an overview of the CODA framework for modelling and refinement of component-based embedded systems. CODA is an extension of Event-B and UML-B and is supported by a plug-in for the Rodin toolset. CODA augments Event-B with constructs for component-based modelling including components, communications ports, port connectors, timed communications and timing triggers. Component beha… ▽ More This paper provides an overview of the CODA framework for modelling and refinement of component-based embedded systems. CODA is an extension of Event-B and UML-B and is supported by a plug-in for the Rodin toolset. CODA augments Event-B with constructs for component-based modelling including components, communications ports, port connectors, timed communications and timing triggers. Component behaviour is specified through a combination of UML-B state machines and Event-B. CODA communications and timing are given an Event-B semantics through translation rules. Refinement is based on Event-B refinement and allows layered construction of CODA models in a consistent way. △ Less

Submitted 27 May, 2013; originally announced May 2013.

Comments: In Proceedings Refine 2013, arXiv:1305.5634

Journal ref: EPTCS 115, 2013, pp. 36-51

Building on the DEPLOY Legacy: Code Generation and Simulation

Authors: Andrew Edmunds, Michael Butler, John Colley

Abstract: The RODIN, and DEPLOY projects laid solid foundations for further theoretical, and practical (methodological and tooling) advances with Event-B. Our current interest is the co-simulation of cyber-physical systems using Event-B. Using this approach we aim to simulate various features of the environment separately, in order to exercise deployable code. This paper has two contributions, the first is… ▽ More The RODIN, and DEPLOY projects laid solid foundations for further theoretical, and practical (methodological and tooling) advances with Event-B. Our current interest is the co-simulation of cyber-physical systems using Event-B. Using this approach we aim to simulate various features of the environment separately, in order to exercise deployable code. This paper has two contributions, the first is the extension of the code generation work of DEPLOY, where we add the ability to generate code from Event-B state-machine diagrams. The second describes how we may use code, generated from state-machines, to simulate the environment, and simulate concurrently executing state-machines, in a single task. We show how we can instrument the code to guide the simulation, by controlling the relative rate that non-deterministic transitions are traversed in the simulation. △ Less

Submitted 25 October, 2012; originally announced October 2012.

Comments: In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in develo** dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012

Creating a level playing field for all symbols in a discretization

Authors: Matthew Butler, Dimitar Kazakov

Abstract: In time series analysis research there is a strong interest in discrete representations of real valued data streams. One approach that emerged over a decade ago and is still considered state-of-the-art is the Symbolic Aggregate Approximation algorithm. This discretization algorithm was the first symbolic approach that mapped a real-valued time series to a symbolic representation that was guarantee… ▽ More In time series analysis research there is a strong interest in discrete representations of real valued data streams. One approach that emerged over a decade ago and is still considered state-of-the-art is the Symbolic Aggregate Approximation algorithm. This discretization algorithm was the first symbolic approach that mapped a real-valued time series to a symbolic representation that was guaranteed to lower-bound Euclidean distance. The interest of this paper concerns the SAX assumption of data being highly Gaussian and the use of the standard normal curve to choose partitions to discretize the data. Though not necessarily, but generally, and certainly in its canonical form, the SAX approach chooses partitions on the standard normal curve that would produce an equal probability for each symbol in a finite alphabet to occur. This procedure is generally valid as a time series is normalized before the rest of the SAX algorithm is applied. However there exists a caveat to this assumption of equi-probability due to the intermediate step of Piecewise Aggregate Approximation (PAA). What we will show in this paper is that when PAA is applied the distribution of the data is indeed altered, resulting in a shrinking standard deviation that is proportional to the number of points used to create a segment of the PAA representation and the degree of auto-correlation within the series. Data that exhibits statistically significant auto-correlation is less affected by this shrinking distribution. As the standard deviation of the data contracts, the mean remains the same, however the distribution is no longer standard normal and therefore the partitions based on the standard normal curve are no longer valid for the assumption of equal probability. △ Less

Submitted 18 October, 2012; originally announced October 2012.

Rewriting and Well-Definedness within a Proof System

Authors: Issam Maamria, Michael Butler

Abstract: Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potent… ▽ More Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B. △ Less

Submitted 22 December, 2010; originally announced December 2010.

Comments: In Proceedings PAR 2010, arXiv:1012.4555

Journal ref: EPTCS 43, 2010, pp. 49-64

Deriving Relationship Between Semantic Models - An Approach for cCSP

Authors: Shamim H. Ripon, Michael Butler

Abstract: Formal semantics offers a complete and rigorous definition of a language. It is important to define different semantic models for a language and different models serve different purposes. Building equivalence between different semantic models of a language strengthen its formal foundation. This paper shows the derivation of denotational semantics from operational semantics of the language cCSP.… ▽ More Formal semantics offers a complete and rigorous definition of a language. It is important to define different semantic models for a language and different models serve different purposes. Building equivalence between different semantic models of a language strengthen its formal foundation. This paper shows the derivation of denotational semantics from operational semantics of the language cCSP. The aim is to show the correspondence between operational and trace semantics. We extract traces from operational rules and use induction over traces to show the correspondence between the two semantics of cCSP. △ Less

Submitted 17 February, 2010; v1 submitted 17 February, 2010; originally announced February 2010.

Comments: 8 Pages IEEE format, International Journal of Computer Science and Information Security, IJCSIS January 2010, ISSN 1947 5500

Report number: Computer Science Volume 7 ISSN 19475500 ACM Class: F.4.1; F.3.2

Journal ref: International Journal of Computer Science and Information Security, IJCSIS, Vol. 7, No. 1, pp. 47-54, January 2010, USA

Formalizing cCSP Synchronous Semantics in PVS

Authors: Shamim H. Ripon, Michael Butler

Abstract: Compensating CSP (cCSP) is a language defined to model long running business transactions within the framework of standard CSP process algebra. In earlier work, we have defined both traces and operational semantics of the language. We have shown the consistency between the two semantic models by defining a relationship between them. Synchronization was missing from the earlier semantic definitio… ▽ More Compensating CSP (cCSP) is a language defined to model long running business transactions within the framework of standard CSP process algebra. In earlier work, we have defined both traces and operational semantics of the language. We have shown the consistency between the two semantic models by defining a relationship between them. Synchronization was missing from the earlier semantic definitions which is an important feature for any process algebra. In this paper, we address this issue by extending the syntax and semantics to support synchronization and define a relationship between the semantic models. Moreover, we improve the scalability of our proof technique by mechanically verifying the semantic relationship using theorem prover PVS. We show how to embed process algebra terms and semantics into PVS and to use these embeddings to prove the semantic relationship. △ Less

Submitted 20 January, 2010; originally announced January 2010.

Comments: 9 pages

ACM Class: F.4.1; F.3.2