Executable specification of P systems with active membranes and its implementation

Based on rewriting logic, an executable specification method was proposed to specify the P systems with active membranes (PSAM) in Maude language. The purpose is to check the correctness of the model automatically and study the properties of PSAM with the help of computer. Six formal specifications were defined in Maude respectively for the six basic rules in PSAM, so that any given PSAM model can be specified formally. An example was presented to demonstrate how to specify the PSAM model, which is used to solve SAT Problem. The feasibility and correctness of the specification method are concluded practically, with the analysis of the result that is reduced by running the specification in Maude.