31 Result(s)
within
Computer Science
Software Engineering
Clare **ks
Conference Paper
-
Chapter and Conference Paper
Efficient Local Reductions to Basic Modal Logic
We present novel reductions of the propositional modal logics , , , ...
-
Chapter and Conference Paper
A Summary of Formal Specification and Verification of Autonomous Robotic Systems
Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are in...
-
Chapter and Conference Paper
Analysing Security Protocols Using Scenario Based Simulation
In this paper, we present a methodology for analysing security protocols using scenario based simulation. A scenario of a potential attack specifies the flow but not the content of messages. Using scenarios c...
-
Chapter and Conference Paper
Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages
Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety
-
Chapter and Conference Paper
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators
Nature-inspired synchronisation protocols have been widely adopted to achieve consensus within wireless sensor networks. We analyse the power consumption of such protocols, particularly the energy required to ...
-
Chapter and Conference Paper
Theorem Proving for Metric Temporal Logic over the Naturals
We study translations from Metric Temporal Logic (MTL) over the natural numbers to Linear Temporal Logic (LTL). In particular, we present two approaches for translating from MTL to LTL which preserve the ExpSpace
-
Chapter and Conference Paper
CRutoN: Automatic Verification of a Robotic Assistant’s Behaviours
The Care-O-bot is an autonomous robotic assistant that can support people in domestic and other environments. The behaviour of the robot can be defined by a set of high level control rules. The adoption and fu...
-
Chapter and Conference Paper
Abstract State Machines and System Theoretic Process Analysis for Safety-Critical Systems
The Abstract State Machine (ASM) method is a formal specification and modeling technique that allows us to specify computational systems at the required abstraction level and facilitates formal analysis and ve...
-
Chapter and Conference Paper
: A Resolution-Based Prover for Multimodal K
In this paper, we describe an implementation of a hyper-resolution-based calculus for the propositional basic multimodal logic,
-
Chapter and Conference Paper
A Modal-Layered Resolution Calculus for K
Resolution-based provers for multimodal normal logics require pruning of the search space for a proof in order to deal with the inherent intractability of the satisfiability problem for such logics. We present...
-
Chapter and Conference Paper
Ordered Resolution for Coalition Logic
In this paper we introduce a calculus based on ordered resolution for Coalition Logic (CL), improving our previous approach based on unrefined resolution, and discuss the problems associated with imposing an orde...
-
Chapter and Conference Paper
An LTL Proof System for Runtime Verification
We propose a local proof system for LTL formalising deductions within the constraints of Runtime Verification (RV), and show how such a system can be used as a basis for the construction of online runtime moni...
-
Chapter and Conference Paper
Clausal Resolution for Modal Logics of Confluence
We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we...
-
Chapter and Conference Paper
Powerchord: Towards Ambient Appliance-Level Electricity Use Feedback through Real-Time Sonification
Feedback on energy use mainly uses visual, numerical interfaces. This paper introduces an alternative: energy sonification, turning real-time electricity use data from appliances into ambient sound. Powerchord, a...
-
Chapter and Conference Paper
Numerical Aspects in the Evaluation of Measurement Uncertainty
Numerical quantification of the results from a measurement uncertainty computation is considered in terms of the inputs to that computation. The primary output is often an approximation to the PDF (probability...
-
Chapter and Conference Paper
Analysis, Redesign and Evaluation with Teasing Apart, Piecing Together
This half-day tutorial will teach participants how and when to use Teasing Apart, Piecing Together (TAPT), a two-phase design method for understanding and redesigning user experiences in new contexts. TAPT was...
-
Chapter and Conference Paper
A Study of User Needs for the ‘Techno Kitchen’
A project, Transitions in Kitchen Living (TiKL) has been conducted to study kitchen histories and current use by older people. A multidisciplinary team developed a common interview methodology to collect peopl...
-
Chapter and Conference Paper
A Formal Semantics for Brahms
The formal analysis of computational processes is by now a well-established field. However, in practical scenarios, the problem of how we can formally verify interactions with humans still remains. In this pap...
-
Chapter and Conference Paper
Taming the Complexity of Temporal Epistemic Reasoning
Temporal logic of knowledge is a combination of temporal and epistemic logic that has been shown to be very useful in areas such as distributed systems, security, and multi-agent systems. However, the complexi...
-
Chapter and Conference Paper
A Refined Resolution Calculus for CTL
In this paper, we present a refined resolution-based calculus for Computation Tree Logic (CTL). The calculus requires a polynomial time computable transformation of an arbitrary CTL formula to an equi-satisfia...
