Search
Now showing items 1-6 of 6
Using ITL and Tempura for large scale specification and simulation.
(IEEE, 1996)
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 ...
Integrating structured OO approaches with formal techniques for the development of real-time systems
(Elsevier, 1999)
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.
(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 ...
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 ...
Refining interval temporal logic specifications
(Springer, 1997)
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 ...
Designing a provably correct robot control system using a "lean" formal method
(Springer, 1998)
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. ...
