Now showing items 1-6 of 6
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 systematic construction of information systems
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 ...
A framework for analysing the effect of "change" in legacy code
We propose a sound and practical approach, based on a formal method (known as Interval Temporal Logic), to cope with “change” and analyse its effect. The approach allows us to capture a snapshot of system’s behaviour over ...
Compositional modelling: The formal perspective
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 ...
Refining interval temporal logic specifications
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
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. ...