Adapting the duty cycle to traffic load in a preamble sampling MAC for WSNs: formal specification and performance evaluation