Communication Systems in ClawZ

Abstract

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{VernonZC10,
  author       = {Michael Vernon and
                  Frank Zeyda and
                  Ana Cavalcanti},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {Communication Systems in ClawZ},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {334--348},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_25},
  doi          = {10.1007/978-3-642-11811-1\_25},
  timestamp    = {Mon, 05 Feb 2024 20:35:41 +0100},
  biburl       = {https://dblp.org/rec/conf/asm/VernonZC10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}