Specification and synthesis in interval temporal logic

Research at the University of East Anglia on high-level behavioural specification and hardware synthesis is focused on the use of the programming language Tempura (an executable subset of interval temporal logic (ITL)). ITL has been shown to be a suitable formalism for specifying digital systems, particularly for systems with time-critical interface protocols. Our work is focused on producing correct-by-construction synthesised circuits from Tempura specifications. Recent work by B. Moszkowski (1993) proposes a compositional proof system for ITL which provides a longer term prospect of an integrated proof and synthesis system within the same logical framework