Communication Systems in ClawZ
We investigate the use of ClawZ, a suite of tools for the verification of implementations of control laws, to construct formal
models for control systems in the area of communications and signal-processing intensive applications. Whereas ClawZ has been
successfully applied to verify control components in avionic systems, special requirements need to be identified and addressed
to extend its use to the aforementioned application domain. This gives rise to several extensions, which we explain and subsequently
validate by constructing the Z model of a software-defined radio communication device. The experience reported provides insight
into general issues surrounding the use and extension of ClawZ.