Formally specifying and checking policies and anomalies in service function chaining