All designs3 presented in this paper have been validated using both Microsoft’s Visual GEC tool (Pedersen and Phillips 2009) and the PRISM model checker (Kwiatkowska et al. 2011), both for the deterministic and stochastic semantics of the CRNs. Visual GEC provides a programming language, LBS, for designing and simulating any given CRN. We systematically tested each component in isolation by simulating its behaviour against all input and output configurations. Next, we examined how a component might behave in a larger system, where it will be exposed to a change in input. To this end, we introduced new reactions to emulate a signal change. For instance, if we wished to change a carrier signal from high to low, we would introduce an additional reaction \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$X_{hi} \overset{k}{\rightarrow } X_{lo}$$\end{document}Xhi→kXlo, which converts all of the signal \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$X_{hi}$$\end{document}Xhi into a signal \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$X_{lo}$$\end{document}Xlo while the component is operating.