A Constrained ECA Language Supporting Formal Verification of WSNs