Now showing items 1-10 of 25
Using ITL and Tempura for large scale specification and simulation.
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 ...
The Enhancement of the Goodyer Skin Rheometer by means of a Microcontroller Based PCB.
(European Design and Test Conference (EDTC) Paris, 1997-03)
GSI Ltd designs and manufactures low volume high cost specialist Test and Measurement Equipment, mainly concentrating on systems for use by the cosmetics industry, and for use in prototype vehicles. The FUSE project involved ...
Integrating structured OO approaches with formal techniques for the development of real-time systems
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 ...
Parallel composition of assumption-commitment specifications: a unifying approach for shared variable and distributed message passing concurrency
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 ...
A wide-spectrum language for object-based development of real-time systems.
(Elsevier Preprints, 1999-03-15)
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 ...
Recursion removal/introduction by formal transformation: an aid to program development and program comprehension
(Oxford University Press, 1999)
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 ...
Proving the correctness of the interlock mechanism in processor design.
(Chapman & Hall on behalf of the International Federation for Information Processing (IFIP), 1997)
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 ...
An intelligent colour graphics display for use in vehicle dashboard instrument clusters.
(2nd International Conference on Road Vehicle Automation (ROVA 95), 1995-09)
The design and implement of computer network for Changchun Telecommunications Bureau.
(Jilin University, 1998)
A dense-time temporal logic with nice compositionality properties
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 ...