随着信息技术日益渗透到人们的日常生活、信息空间与物理空间的日趋融合,计算技术正在改变着我们的生存环境。与此同时,人们对信息科学的依赖达到了前所未有程度,对于信息科学及其数学基础的需求也变得越来越迫切。如何为诸如Internet、普适计算等大规模复杂系统提供一个计算模型,并且,该模型不但可以分析现存的软件系统而且能够指导软件系统的规约、设计、编程,以及在不损坏软件系统的情况下对其进行改造升级。另外,现存的进程演算在刻画并行进程的互连、移动进程的连通性以及进程的空间位置、移动等方面都取得了很大的进展。尽管这些演算的基本观点和理论—特别是对行为规约、行为等价关系的理解等方面—存在着某些相似之处,但它们缺少一个统一的形式,没有固定的方式将几种不同的移动性组合在一起。如何为并发和移动进程理论提供一个元模型是进程演算面临的重大挑战。面对应用与理论方面的挑战,Robin及其合作者提出了Bigraph理论。该理论是一种基于图形的形式化理论工具,同时强调了计算(物理或虚拟)的位置移动和移动的联通性,是比传统移动进程演算更一般的理论。为了更好地为进程演算提供一个元语言以及更好地理解并刻画普适计算等系统,许多学者从不同的角度提出了Bigraph理论的扩展模型。本论文就是针对Bigraph位置图中控制间的嵌套关系、连接图中的连接匹配等问题,提出了一个赋类的Bigraph扩展模型并给出了它的两个重要应用。本论文的主要工作如下：1.提出了一个基于赋类的Bigraph扩展模型一定型Bigraph。它是嵌套赋类位置图BGsortP与斑点赋类连接图BGsortL两者组合而成的BGsort=〈BGsortP, BGsortL〉。·对于嵌套赋类位置图：在利用标签范畴Scat(Κ)给出嵌套赋类位置图定义的基础上,讨论了嵌套赋类位置图的相关性质,给出了嵌套赋类位置图中RPO的构建、证明,同前推出IPO的一致性条件的定义、证明等。●对于斑点赋类连接图：通过对Bigraph位置图中的斑点进行类型指派,给出了斑点间类型匹配规则以及斑点赋类连接图的定义。与嵌套赋类位置图一样,也对其关键特性进行了讨论。●对于组合的定型Bigraph:除了与纯Bigraph中相应概念的比较外,也给出了定型Bigraph中的重要定义和命题。2.将定型Bigraph作为元语言对面向行为的软件需求建模语言(BDL)进行了描述。本研究扩展了Bigraph作为进程演算元模型的应用范围,展示了其在描述需求演算方面的能力,为在Bigraph框架下研究需求演算奠定了基础。·对BDL语言进行了精化规约,定义了BDLRef的标准型、互模拟关系。●定义了有限BDLRef在Bigraph描述中的嵌套赋类、斑点赋类的规范,给出了有限BDLRef到其Bigraph描述的转换映射BehExfmap、Mmap,证明了转换映射的对应关系。在此基础上,讨论了BG-BDLRef的反应系统及其衍生的标号迁移系统。●利用Bigraph生长理论对BDLRef的动作常量BehCons进行了Bigraph描述。3.定型Bigraph理论在普适计算上下文感知系统中的应用。●给出了定型Bigraph理论中带有演算行为的Bigraph反应系统。实质上,带演算的BRS是演算反应→与常规反应→两个系统的组合。在给出演算BRS的定义及其相关特性的基础上,讨论了→与→之间的关系,证明了在带演算的BRS中展开反应是交汇的,并且能够产生但是不会破坏或妨碍常规反应关系。●讨论了利用带演算的BRS对上下文感知系统进行建模的方法。并且通过对经典实例的建模与已有上下文感知系统的Bigraph模型一柏拉图图形模型一进行了比较,展示了带演算的Bigraph反应系统在上下文感知系统建模方面的表达能力。