We are currently developing tool support for the CCM modeling formalism with the goal of applying HCOS techniques to several variants of Linux, including SMP, Beowulf, and embedded Linux. To date, a prototype has been implemented that consists of a visual front-end for interactive specification using CCMs, and automatic generation of Java code for most CCM features. Other tools developed for the analysis of non-CCM operational models are also being retargeted to CCMs.