Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude