-
Urgency Annotations for Alternating Choices
Authors:
Eren Keskin,
Roland Meyer,
Sören van der Wall
Abstract:
We propose urgency programs, a new programming model with support for alternation, imperfect information, and recursion. The novelty are urgency annotations that decorate the (angelic and demonic) choice operators and control the order in which alternation is resolved. We study standard notions of contextual equivalence for urgency programs. Our first main result are fully abstract characterizatio…
▽ More
We propose urgency programs, a new programming model with support for alternation, imperfect information, and recursion. The novelty are urgency annotations that decorate the (angelic and demonic) choice operators and control the order in which alternation is resolved. We study standard notions of contextual equivalence for urgency programs. Our first main result are fully abstract characterizations of these relations based on sound and complete axiomatizations. Our second main result settles their computability via a normal form construction. Notably, we show that the contextual preorder is (2h-1)-EXPTIME-complete for programs of maximal urgency h when the regular observable is given as an input resp. PTIME-complete when the regular observable is fixed. We designed urgency programs as a framework in which it is convenient to formulate and study verification and synthesis problems. We demonstrate this on a number of examples including the verification of concurrent and recursive programs and hyper model checking.
△ Less
Submitted 20 October, 2023; v1 submitted 4 May, 2023;
originally announced May 2023.
-
Model-based Fault Classification for Automotive Software
Authors:
Mike Becker,
Roland Meyer,
Tobias Runge,
Ina Schaefer,
Sören van der Wall,
Sebastian Wolff
Abstract:
Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a crucial and labor intensive task to the test engineer: identifying bugs in failing tests. Our contribution is a model-based classification algorithm for failing tests that assists the engineer when identifying bugs. It consis…
▽ More
Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a crucial and labor intensive task to the test engineer: identifying bugs in failing tests. Our contribution is a model-based classification algorithm for failing tests that assists the engineer when identifying bugs. It consists of three steps. (i) Fault localization replays the test on the model to identify the moment when the two diverge. (ii) Fault explanation then computes the reason for the divergence. The reason is a subset of actions from the test that is sufficient for divergence. (iii) Fault classification groups together tests that fail for similar reasons. Our approach relies on machinery from formal methods: (i) symbolic execution, (ii) Hoare logic and a new relationship between the intermediary assertions constructed for a test, and (iii) a new relationship among Hoare proofs. A crucial aspect in automotive software is timing requirements, for which we develop appropriate Hoare logic theory. We also briefly report on our prototype implementation for the CAN bus Unified Diagnostic Services in an industrial project.
△ Less
Submitted 15 December, 2022; v1 submitted 30 August, 2022;
originally announced August 2022.
-
All-Chalcogenide Programmable All-Optical Deep Neural Networks
Authors:
Ting Yu,
Xiaoxuan Ma,
Ernest Pastor,
Jonathan K. George,
Simon Wall,
Mario Miscuglio,
Robert E. Simpson,
Volker J. Sorger
Abstract:
Deeplearning algorithms are revolutionising many aspects of modern life. Typically, they are implemented in CMOS-based hardware with severely limited memory access times and inefficient data-routing. All-optical neural networks without any electro-optic conversions could alleviate these shortcomings. However, an all-optical nonlinear activation function, which is a vital building block for optical…
▽ More
Deeplearning algorithms are revolutionising many aspects of modern life. Typically, they are implemented in CMOS-based hardware with severely limited memory access times and inefficient data-routing. All-optical neural networks without any electro-optic conversions could alleviate these shortcomings. However, an all-optical nonlinear activation function, which is a vital building block for optical neural networks, needs to be developed efficiently on-chip. Here, we introduce and demonstrate both optical synapse weighting and all-optical nonlinear thresholding using two different effects in a chalcogenide material photonic platform. We show how the structural phase transitions in a wide-bandgap phase-change material enables storing the neural network weights via non-volatile photonic memory, whilst resonant bond destabilisation is used as a nonlinear activation threshold without changing the material. These two different transitions within chalcogenides enable programmable neural networks with near-zero static power consumption once trained, in addition to picosecond delays performing inference tasks not limited by wire charging that limit electrical circuits; for instance, we show that nanosecond-order weight programming and near-instantaneous weight updates enable accurate inference tasks within 20 picoseconds in a 3-layer all-optical neural network. Optical neural networks that bypass electro-optic conversion altogether hold promise for network-edge machine learning applications where decision-making in real-time are critical, such as for autonomous vehicles or navigation systems such as signal pre-processing of LIDAR systems.
△ Less
Submitted 27 February, 2021; v1 submitted 20 February, 2021;
originally announced February 2021.
-
Resolving the cybersecurity Data Sharing Paradox to scale up cybersecurity via a co-production approach towards data sharing
Authors:
Amir Atapour-Abarghouei,
Andrew Stephen McGough,
David Stanley Wall
Abstract:
As cybercriminals scale up their operations to increase their profits or inflict greater harm, we argue that there is an equal need to respond to their threats by scaling up cybersecurity. To achieve this goal, we have to develop a co-productive approach towards data collection and sharing by overcoming the cybersecurity data sharing paradox. This is where we all agree on the definition of the pro…
▽ More
As cybercriminals scale up their operations to increase their profits or inflict greater harm, we argue that there is an equal need to respond to their threats by scaling up cybersecurity. To achieve this goal, we have to develop a co-productive approach towards data collection and sharing by overcoming the cybersecurity data sharing paradox. This is where we all agree on the definition of the problem and end goal (improving cybersecurity and getting rid of cybercrime), but we disagree about how to achieve it and fail to work together efficiently. At the core of this paradox is the observation that public interests differ from private interests. As a result, industry and law enforcement take different approaches to the cybersecurity problem as they seek to resolve incidents in their own interests, which manifests in different data sharing practices between both and also other interested parties, such as cybersecurity researchers. The big question we ask is can these interests be reconciled to develop an interdisciplinary approach towards co-operation and sharing data. In essence, all three will have to co-own the problem in order to co-produce a solution. We argue that a few operational models with good practices exist that provide guides to a possible solution, especially multiple third-party ownership organisations which consolidate, anonymise and analyse data. To take this forward, we suggest the practical solution of organising co-productive data collection on a sectoral basis, but acknowledge that common standards for data collection will also have to be developed and agreed upon. We propose an initial set of best practices for building collaborations and sharing data and argue that these best practices need to be developed and standardised in order to mitigate the paradox.
△ Less
Submitted 20 November, 2020;
originally announced November 2020.
