Showing 1–7 of 7 results for author: Jones, C B

Data reification in a concurrent rely-guarantee algebra

Authors: Larissa A. Meinicke, Ian J. Hayes, Cliff B. Jones

Abstract: Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of programs that use more efficient concrete representations. Data reification (or "refinement") techniques for sequential programs are well established. This paper applies these ideas to concurrency, in particular, an algebraic t… ▽ More Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of programs that use more efficient concrete representations. Data reification (or "refinement") techniques for sequential programs are well established. This paper applies these ideas to concurrency, in particular, an algebraic theory supporting rely-guarantee reasoning about concurrency. A concurrent version of the Galler-Fischer equivalence relation data structure is used as an example. △ Less

Submitted 9 May, 2024; originally announced May 2024.

ACM Class: F.3.1; D.1.3

Extending Rely-Guarantee thinking to handle Real-Time Scheduling

Authors: Cliff B. Jones, Alan Burns

Abstract: The reference point for develo** any artefact is its specification; to develop software formally, a formal specification is required. For sequential programs, pre and post conditions (together with abstract objects) suffice; rely and guarantee conditions extend the scope of formal development approaches to tackle concurrency. In addition, real-time systems need ways of both requiring progress an… ▽ More The reference point for develo** any artefact is its specification; to develop software formally, a formal specification is required. For sequential programs, pre and post conditions (together with abstract objects) suffice; rely and guarantee conditions extend the scope of formal development approaches to tackle concurrency. In addition, real-time systems need ways of both requiring progress and relating that progress to some notion of time. This paper extends rely-guarantee ideas to cope with specifications of -- and assumptions about -- real-time schedulers. Furthermore it shows how the approach helps identify and specify fault-tolerance aspects of such schedulers by systematically challenging the assumptions. △ Less

Submitted 30 November, 2023; originally announced December 2023.

Comments: Published on-line (2023-11-30) in "Formal Methods in System Design"

ACM Class: D.2; F.3

Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols

Authors: Nisansala P. Yatapanage, Cliff B. Jones

Abstract: The verification of security protocols is essential, in order to ensure the absence of potential attacks. However, verification results are only valid with respect to the assumptions under which the verification was performed. These assumptions are often hidden and are difficult to identify, making it unclear whether a given protocol is safe to deploy into a particular environment. Rely/guarantee… ▽ More The verification of security protocols is essential, in order to ensure the absence of potential attacks. However, verification results are only valid with respect to the assumptions under which the verification was performed. These assumptions are often hidden and are difficult to identify, making it unclear whether a given protocol is safe to deploy into a particular environment. Rely/guarantee provides a mechanism for abstractly reasoning about the interference from the environment. Using this approach, the assumptions are made clear and precise. This paper investigates this approach on the Needham-Schroeder Public Key protocol, showing that the technique can effectively uncover the assumptions under which the protocol can withstand attacks from intruders. △ Less

Submitted 25 November, 2023; originally announced November 2023.

A Rely-Guarantee Specification of Mixed-Criticality Scheduling

Authors: Cliff B Jones, Alan Burns

Abstract: The application considered is mixed-criticality scheduling. The core formal approaches used are Rely-Guarantee conditions and the Timeband framework; these are applied to give a layered description of job scheduling which includes resilience to jobs overrunning their expected execution time. A novel formal modelling idea is proposed to handle the relationship between actual time and its approximat… ▽ More The application considered is mixed-criticality scheduling. The core formal approaches used are Rely-Guarantee conditions and the Timeband framework; these are applied to give a layered description of job scheduling which includes resilience to jobs overrunning their expected execution time. A novel formal modelling idea is proposed to handle the relationship between actual time and its approximation in hardware clocks. △ Less

Submitted 21 August, 2021; v1 submitted 2 December, 2020; originally announced December 2020.

Comments: This paper will appear in a Festschrift - on publication we will insert a pointer to the book

Journal ref: Mathematical Foundations of Software Engineering, College Publication, 2022, Chap 6

The development and deployment of formal methods in the UK

Authors: Cliff B. Jones, Martyn Thomas

Abstract: UK researchers have made major contributions to the technical ideas underpinning formal approaches to the specification and development of computer systems. Perhaps as a consequence of this, some of the significant attempts to deploy theoretical ideas into practical environments have taken place in the UK. The authors of this paper have been involved in formal methods for many years and both have… ▽ More UK researchers have made major contributions to the technical ideas underpinning formal approaches to the specification and development of computer systems. Perhaps as a consequence of this, some of the significant attempts to deploy theoretical ideas into practical environments have taken place in the UK. The authors of this paper have been involved in formal methods for many years and both have tracked a significant proportion of the whole story. This paper both lists key ideas and indicates where attempts were made to use the ideas in practice. Not all of these deployment stories have been a complete success and an attempt is made to tease out lessons that influence the probability of long-term impact. △ Less

Submitted 24 January, 2021; v1 submitted 11 June, 2020; originally announced June 2020.

Comments: This work has been submitted to the IEEE for possible publication. Copyright may be transferred without notice, after which this version may no longer be accessible

Journal ref: Formal Aspects of Computing, 2022, Vol 34, No 1

Embedding Geographic Locations for Modelling the Natural Environment using Flickr Tags and Structured Data

Authors: Shelan S. Jeawak, Christopher B. Jones, Steven Schockaert

Abstract: Meta-data from photo-sharing websites such as Flickr can be used to obtain rich bag-of-words descriptions of geographic locations, which have proven valuable, among others, for modelling and predicting ecological features. One important insight from previous work is that the descriptions obtained from Flickr tend to be complementary to the structured information that is available from traditional… ▽ More Meta-data from photo-sharing websites such as Flickr can be used to obtain rich bag-of-words descriptions of geographic locations, which have proven valuable, among others, for modelling and predicting ecological features. One important insight from previous work is that the descriptions obtained from Flickr tend to be complementary to the structured information that is available from traditional scientific resources. To better integrate these two diverse sources of information, in this paper we consider a method for learning vector space embeddings of geographic locations. We show experimentally that this method improves on existing approaches, especially in cases where structured information is available. △ Less

Submitted 12 October, 2018; originally announced October 2018.

Possible values: exploring a concept for concurrency

Authors: Cliff B. Jones, Ian J. Hayes

Abstract: An important issue in concurrency is interference. This issue manifests itself in both shared-variable and communication-based concurrency --- this paper focusses on the former case where interference is caused by the environment of a process changing the values of shared variables. Rely/guarantee approaches have been shown to be useful in specifying and reasoning compositionally about concurrent… ▽ More An important issue in concurrency is interference. This issue manifests itself in both shared-variable and communication-based concurrency --- this paper focusses on the former case where interference is caused by the environment of a process changing the values of shared variables. Rely/guarantee approaches have been shown to be useful in specifying and reasoning compositionally about concurrent programs. This paper explores the use of a "possible values" notation for reasoning about variables whose values can be changed multiple times by interference. Apart from the value of this concept in providing clear specifications, it offers a principled way of avoiding the need for some auxiliary (or ghost) variables whose unwise use can destroy compositionality. △ Less

Submitted 9 January, 2016; originally announced January 2016.