An active network describes a new generation of network where all network nodes are programmable. Nodes can be configured according to user requirements at booting or on-the-fly, and each node can also provide computational capabilities to process regular data carrying packets. The flexibility gained in the dynamics of active networks gives rise to significant security and safety issues. In this thesis, we apply Formal Methods to the specification of an active node. The specification process consists of designing a formal framework and then evaluating it. Constructive and axiomatic specifications are used during the design. Evaluation of the framework is achieved by building a working node model and verifying that the model demonstrates the critical properties of an active node. The formal framework and model are both written in the Prototype Verification System (PVS) language. The PVS theorem prover is then used for verifying and validating the proposed model.