Our results concern using program-slicing to model software components in a CPS, with applications to verification of aviation software.