DocumentCode :
288054
Title :
Specification and synthesis in interval temporal logic
Author :
Marshall, I.
Author_Institution :
East Anglia Univ., UK
fYear :
1994
fDate :
1994
Firstpage :
42461
Lastpage :
42463
Abstract :
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
Keywords :
formal specification; temporal logic; Tempura specifications; compositional proof system; correct-by-construction synthesised circuits; hardware synthesis; high-level behavioural specification; interval temporal logic (ITL); programming language Tempura; time-critical interface protocols;
fLanguage :
English
Publisher :
iet
Conference_Titel :
Structured Methods for Hardware Systems Design, IEE Colloquium on
Conference_Location :
London
Type :
conf
Filename :
369632
Link To Document :
بازگشت