Browsing School of Computer Science and Informatics by Submission Date
Now showing items 1-20 of 2592
-
Using PVS for Interval Temporal Logic proofs, part 1: The syntactic and semantic encoding
(Technical Report)Interval temporal logic (ITL) is a logic that is used to specify and reason about systems. The logic has a powerful proof system but rather than doing proofs by hand, which is tedious and error prone, we want a tool that ... -
A definition of abstraction.
(Article)What does it mean to say that one program is "more abstract" than another? What is "abstract" about an abstract data type? What is the difference between a "high-level" program and a "low-level" program? In this paper we ... -
Parallel composition of assumption-commitment specifications: a unifying approach for shared variable and distributed message passing concurrency
(Article)We unify the parallel composition rule of assumption-commitment specifications for respectively state-based and message-based concurrent processes. Without providing language-dependent definitions, we first assume that the ... -
Integrating structured OO approaches with formal techniques for the development of real-time systems
(Article)The use of formal methods in the development of time-critical applications is essential if we want to achieve a high level of assurance in them. However, these methods have not yet been widely accepted in industry as ... -
A wide-spectrum language for object-based development of real-time systems.
(Article)A formal design notation is present whose underlying computational model is object-based. The object structure of the model is based on the practical, industry-strength Object Oriented structure development technique ... -
ATOM: an object-based formal method for real-time systems
(Article)An object based formal method for the development of real-time systems, called ATOM, is presented. The method is an integration of the real-time formal technique TAM (Temporal Agent Model) with an industry-strength structured ... -
Compositional modelling: The formal perspective
(Article)We provide a formal framework within which an Information System (IS) could be modelled, analysed, and verified in a compositional manner. Our work is based on Interval Temporal Logic (ITL) and its programming language ... -
A dense-time temporal logic with nice compositionality properties
(Article)A dense temporal logic specification method for the development of reactive systems is introduced. The two development constructs of this method are refinement and composition. A reactive system is specified by a pair ... -
Formal methods to aid the evolution of software.
(Article)There is a vast collection of operational software systems which are vitally important to their users, yet are becoming increasingly difficult to maintain, enhance and keep up to date with rapidly changing requirements. ... -
Assembler to C migration using the FermaT transformation system
(Article)The FermaT transformation system, based on research carried out over the last twelve years at Durham University and Software Migrations Ltd., is an industrial-strength formal transformation engine with many applications ... -
Refining interval temporal logic specifications
(Book chapter)Interval Temporal Logic (ITL) was designed as a tool for the specification and verification of systems. The development of an executable subset of ITL, namely Tempura, was an important step in the use of temporal logic as ... -
Formal methods for legacy systems.
(Article)A method is described for obtaining useful information from legacy code. The approach uses formal proven program transformations, which preserve for refine the semantics of a construct while changing its form. The applicability ... -
Using ITL and Tempura for large scale specification and simulation.
(Book chapter)ITL and Tempura are used for respectively the formal specification and simulation of a large scale system, namely the general purpose multi-threaded dataflow processor EP/3. This paper shows that this processor can be ... -
Proving the correctness of the interlock mechanism in processor design.
(Book chapter)In this paper, Interval Temporal Logic (ITL) us used to specify and verify the event processor EP/3, which is a multi-threaded pipeline processor capable of executing parallel programs. We first give the high level ... -
Recursion removal/introduction by formal transformation: an aid to program development and program comprehension
(Article)The transformation of a recursive program to an iterative equivalent is a fundamental operation in Computer Science. In the reverse direction, the task of reverse engineering (analysing a given program in order to determine ... -
Designing a provably correct robot control system using a "lean" formal method
(Book chapter)A development method for the construction of provably correct robot control systems together with its supporting tool environment are described. The method consists of four stages: 1. specification, 2. refinement, 3. ... -
Compositional verification and specification of refinement for reactive systems in a dense time temporal logic
(Thesis)This thesis introduces a compostitional dense time temporal logic for the compositions and refinement of reactive systems. A reactive system is specified by a pair consisting of a machine and a condition on the computations ... -
Derivation of data intensive algorithms by formal transformation: the Schorr-Waite graph marking algorithm
(Article)In this paper we consider a particular class of algorithms which present certain difficulties to formal verification. These are algorithms which use a single data structure for two or more purposes, which combine program ... -
The systematic construction of information systems
(Book chapter)Process modelling is a vital issue for communicating with experts of the application domain. Depending on the roles and responsibilities of the application domain experts involved, process models are discussed on different ... -
Program analysis by formal transformation
(Article)This paper treats Knuth and Szwarcfiter’s topological sorting program, presented in their paper “A structured program to generate all topological sorting arrangements” (Knuth and Szwarcfiter 1974), as a case study for the ...