This paper presents a natural algebraic specification for the P systems. The specification is executable in Maude, a software system supporting rewriting and equational logic. We define the P system maximal parallel evolution as a specific rewriting strategy in Maude. By extending the Maude rewriting semantics with this strategy, we provide an operational semantics of the P systems. We present few examples of specifying and executing simple P systems, describing how target indications, dissolving and priorities are handled. Moreover, the Maude system allows the verification of various properties of the P systems expressed as linear temporal logic formulas by using a model checker.