Their was a paper discussing the Z notational form in the specification of the 744 RR FADEC... I read it at University sad git that I am. I think it may have been published by the Computing Unit (Oxford Uni). I will try and find it for you.
The Spec obviously should encompass the design.