- DORA Home
- →
- Faculty of Technology
- →
- School of Computer Science and Informatics
- →
- Browsing School of Computer Science and Informatics by Submission Date
JavaScript is disabled for your browser. Some features of this site may not work without it.
Browse
My Account
Browsing School of Computer Science and Informatics by Submission Date
Now showing items 1-20 of 2341
-
(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 ...
-
(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 ...
-
(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 ...
-
(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 ...
-
(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 ...
-
(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 ...
-
(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 ...
-
(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. ...
-
(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 ...
-
(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 ...
-
(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 ...
-
(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 ...
-
(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 ...
-
(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 ...
-
(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. ...
-
(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 ...
-
(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 ...
-
(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 ...
-
(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 ...
Now showing items 1-20 of 2341
