XYZ is a software engineering system consisting of a temporal logic language XYZ/ E and a set of CASEtools.The temporal logic language XYZ/ E is based on Manna- Pnuli's Linear- Time Temporal L ogic.It canrepresent both high level and low level specifications in the same frame work,so that the specification andimplementation of software systems are very convenient.XYZ/ E is simple yet expressive enough to be acceptedby engineers.Besides,the formal nature of this language makes it capable of programming verif...