随着计算机科学与其他学科之间的相互渗透和影响,科学家们根据不同原理提出了不同的计算模型。细胞膜计算是一种基于生物细胞膜结构和功能的新型计算模型,近年来得到广泛的研究。SN P系统(Spiking Neural P Systems)是对类神经细胞膜计算(Neural-like P Systems)的扩展。与其他细胞膜计算的不同的是,它在计算中引入了时间的概念,计算由一个全局时钟驱动。SN P系统已被证明具有与图灵机相同的计算能力。然而随着研究的深入,模型的设计越来越复杂,如何有效地验证模型的正确性和研究SN P系统的性质成为该领域当前一个迫切需要解决的问题。模型检测作为一种研究和验证系统性质的方法,可以有效地帮助我们解决这一问题。目前用于模型检测的工具主要有SPIN、Maude等。Maude是一种基于重写逻辑的形式化描述语言,由Maude解释器解释执行,主要用于模型检测和逻辑推理。[0]本文的主要工作是:通过扩展Maude中的重写规则语义,利用代数方法定义了SN P系统中计算规则的操作语义,并借助于Maude中面向对象的形式化描述,给出了SN P系统通用的描述方法,把SN P系统转化成为可执行的形式化描述。这种形式化的描述可以被Maude解释器解释运行,从而自动推导系统的计算结果、验证系统的某些性质等。最后,本文将这一形式化描述方法应用于具体的SN P系统模型并给出了验证的结果,证明了模型检测的可行性与正确性。本文的主要贡献是:将模型检测应用于SN P系统;利用Maude语言定义了SN P系统中计算规则的操作语义;给出了SN P系统在Maude下通用的形式化描述方法;达到了通过计算机辅助验证SN P系统正确性与完整性[0]的目的。