Membrane systems are a biologically-inspired computational model based on the structure of biological cells and the way chemicals interact and traverse their membranes. Although their dynamics are described by rules, encoding membrane systems into rewriting logic is not straightforward due to its complex control mechanisms. Multiple alternatives have been proposed in the literature and implemented in the Maude specification language. The recent release of the Maude strategy language and its associated strategy-aware model checker allow specifying these systems more easily, so that they become executable and verifiable for free. An easily-extensible interactive environment transforms membrane specifications into rewrite theories controlled by appropriate strategies, and allows simulating and verifying membrane computations by means of them.

翻译：膜系统是一种受生物细胞结构及化学物质相互作用与跨膜运输方式启发的计算模型。尽管其动态行为由规则描述，但由于其复杂的控制机制，将膜系统编码为重写逻辑并非易事。文献中已提出多种替代方案，并在Maude规范语言中实现。最新发布的Maude策略语言及其配套的策略感知模型检验器，使得这些系统的描述更加简便，从而使其可自动执行与验证。一个易于扩展的交互式环境可将膜系统规范转化为由适当策略控制的重写理论，并借助这些策略实现对膜计算的仿真与验证。