Many different notions of "program property", and many different methods of verifying such properties, arise naturally in programming. We present a general framework of Specification Structures for combining different notions and methods in a coherent fashion. We then apply the idea of specification structures to concurrency in the setting of Interaction Categories. As a specific example, a certain specification structure defined over the interaction category SProc yields a new category SProcD whose type system is strong enough to guarantee deadlock-freedom of concurrent processes. We present some techniques for manipulating typed processes in this category, and show that they allow us to reason about deadlock-freedom in synchronous networks, a class of concurrent systems which incorporates both synchronous dataflow programs and systolic algorithms.