理论计算机科学电子笔记97（2004）259-276www.elsevier.com/locate/entcs移动环境下的上下文感知推理Christine Julien，Jamie Payton和Gruia-Catalin Roman1移动计算实验室计算机科学与工程美国密苏里州圣路易斯华盛顿大学摘要上下文感知正在成为一个重要的计算范例，旨在解决应用程序的特殊需求，必须适应或利用高度动态的环境中出现的物理或逻辑的移动性。有许多形式化的模型可用于对并发性进行推理。旨在捕捉流动性特 征的 模型 较少 ，但 仍具有 良好 的代 表性 （例 如，Mobile Ambients、 π-Calculus和 MobileUNITY）。 然而，这些模型不提供上下文感知交互的显式建模所需的构造。本文建立在早期的基于状态的正式推理的移动性和探索的过程中，一个模型，如移动UNITY可以转换为显式捕获上下文感知。从上下文感知系统的基本特征的检查，本文探讨了一系列的结构，旨在促进高度解耦的风格的编程上下文感知组件。这种探索的结果是一个称为上下文统一的模型。关键词：形式化方法，上下文感知，移动计算，统一，上下文统一，共享变量1介绍形式模型有助于理解编程任务的本质，例如，通过允许指定和验证程序第一个正规编程模型专注于顺序编程。例如，Floyd [10霍尔三元组[12]允许通过使用预-1电子邮件：{julien，payton，roman}@ wustl.edu1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.040260C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276后的条件。随着焦点转向并发编程，出现了这种独特环境的新模型。例如，CSP [13]和CCS [17]从代数的角度来处理并发系统。它们使用进程和同步通信来建模系统与其环境之间的交互。UNITY模型[5]通过推理程序状态的转换来最近，并发编程模型已被调整，以考虑到环境的复杂性，需要物理和/或逻辑的移动性。π演算[18]建立在CCS的基础上，作为通信系统的进程代数，允许表达可重构的移动进程。Mobile Ambients[4]对管理域之间的流程Mobile UNITY [23]扩展了UNITY，使其能够在日志空间中捕获位置和移动，并促进了对移动程序的断言式推理。（由于Mobile UNITY是这项工作的基础，我们将在第3节中详细讨论它。随着新的编程范例的出现，并不总是需要发明新的符号和模型。类似环境的模型的先前工作可以通过两种方式之一来重用：通过将新的范例减少到已经存在的模型，或者通过将现有的模型专门化到新的范例。例如，移动计算共享了并发编程的许多特征事实上，移动计算范式本身就是并发编程范式的扩展由于这个原因，并发编程模型对移动计算环境的适应被证明是成功的，例如，π演算扩展CCS和Mobile UNITY专用UNITY。这种专门化有助于提供所需的结构，而与既定模式的连续性则允许在系统的分析和评价中重新利用先前的知识进步。上下文感知计算是一种重要的新兴计算模式，它使移动程序能够根据环境的变化来调整自己的行为。直接重用移动性的正式模型会妨碍基于上下文的交互的简单指定，因为原语是为移动交互量身定制的。然而，由于上下文感知应用程序通常在移动环境中运行，因此调整这样的移动性模型以考虑上下文感知交互允许我们重用证明逻辑的移动性构造和部分。我们的方法专门移动统一提供的结构，允许推理的操纵和与上下文的交互。结果模型Context UNITY继承了Mobile UNITY的许多功能，包括其符号和证明逻辑。第2节回顾了移动程序C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276261目前的系统和应用。第3节简要回顾了Mobile UNITY模型。第4节概述了上下文统一的基本概念，并通过一个简单的上下文感知系统给出了它的形式化。最后，讨论见第5节，结论见第6节。2上下文感知计算移动计算应用程序需要连接的主机通过无线连接交换数据的能力。物理上移动的主机形成一个拓扑结构不断变化的网络。这种高度动态的物理结构支持一种由具有在移动主机之间移动能力的应用级组件组成的更加灵活的逻辑结构。由于不断变化的环境，应用程序经常表现出机会主义的、高度自适应的、并且非常依赖于资源的可用性的能力，这些资源在本质上也可能是瞬时的许多研究人员提倡上下文感知计算，或应用程序能够检测其环境中的变化并调整其行为以响应这些变化[26]。这一领域的初步工作集中在位置感知上，并允许程序根据身体运动调整其行为[11，27]。然而，最近，感知上下文的应用和系统已经开始包括环境的更多变化的方面最值得注意的是，上下文工具包[25]允许定义可以感知环境中任意因素的上下文小部件。事实上，正如[20]所提出的，我们最初视为数据内容的内容也可能是用户上下文的一部分存在许多用于收集和传播上下文信息的系统一些应用程序在[1，3，6，9，22，24]中内置了这些设施，而其他工作则专注于构建中间件支持系统，通过订阅-订阅结构[7]或通过基于状态的交互[14，19]来分发上下文信息。我们对上下文的看法侧重于为应用程序提供灵活的机制，以定义随着环境变化而透明维护的个性化上下文。这种上下文视图包含当前应用程序和系统所使用的定义。回顾一下，上下文由连接设备上的任何可用信息（传统上下文信息和任意数据）定义。 我们的上下文定义的最重要的方面之一来自于观察，即各个应用程序需要来自其环境的不同事物。出于这个原因，我们从一个单一的组成部分的角度来定义上下文，采取自我中心的世界观。这一决定的关键分歧是，262C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276组件“看到”相同的上下文。由于目标环境中包含许多连接的移动主机，我们扩展了这个上下文的边界，不仅包含本地主机感测到的信息，而且还包含任何连接的主机上的信息。虽然上下文感知计算的系统和应用程序的可用性已经迅速增加，但还没有出现用于其行为的正式模型。现在是时候从形式化的角度来探索上下文感知了。所得到的模型的符号和证明逻辑应该有助于推理上下文感知程序的形式，但该模型应该足够类似于实际的编程语言，很容易过渡到一个实现。在下一节中，我们将回顾移动UNITY模型，我们的上下文UNITY基于该模型。3Mobile UNITY本节通过一个具体的例子对Mobile UNITY进行了简单的介绍。 有兴趣更详细地解释该模型[23]及其在移动IP规范和验证[16]以及移动代码建模和验证[21]中的应用的读者可以使用大量已发表的工作。Mobile UNITY基于Chandy和Misra的UNITY模型[5]，扩展了符号和证明逻辑。图1显示了一个名为BaggageTransfer的Mobile UNITY系统。这种类型的系统如图2所示。在这个系统中，定义了三个程序，它们结合并相互作用，形成一个系统，在该系统中，推车在装载机和卸载机之间运送货物在一维轨道上，其中装载机在轨道的左侧，并且卸载机在右侧。Cart（k）定义了一个程序，在这个程序中行李车沿着轨道移动。 在UNITY中，程序规范的关键元素是变量和赋值。程序是一组条件赋值语句，由符号[]分隔。每个语句都以原子方式执行，并以弱公平的方式选择执行-在无限计算中，每个语句都计划以无限的频率执行。任何正常语句（相对于反应语句和抑制语句）的保护都可以通过使用抑制语句来加强，而无需修改语句。MobileUNITY的一个独特构造是可以触发的反应语句1非确定性赋值语句[2]x：=x′.Q将从满足谓词Q的值中非确定性地选择的值x′赋值给x。2虽然它的语义与if关键字相同，但when关键字在Mobile UNITY系统的交互C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276263Fig. 1. 示例Mobile UNITY系统图二、由推车、装载机和卸载机组成的系统一个先决条件。在操作上，我们可以把每一个赋值都看作是通过执行所有定义的反应而扩展的，直到这样一个点，即仅仅执行反应就不可能有进一步的状态变化更正式地说，所有反应式语句的集合形成了一个程序，它被执行为固定的。每一个原子状态的变化。很明显，他必须是一个终结者-将通过示例系统更详细地解释抑制语句和反应语句。Cart（k）在declare部分定义变量x类型的整数;x表示cart的负载大小每个Mobile UNITY程序也有一个位置，由区别变量λ表示;此变量在Mobile UNITY模型之外初始部分声明在执行开始时购物车是注意，λ没有显式初始化;它可以在程序执行开始时取任何整数值此外，虽然这个例子使用了一个简单的一维空间概念，这个模型并没有限制系统对空间的定义。Cart（k）的分配部分说明了几种Mobile UNITY结构的使用陈述正确系统行李转移程序Cart（k）在λ宣布x：整数最初x= 0时分配向右：：λ：=λ+1[]向左 ：：λ：=λ−1[]inhibitgorightwhenx=0[]inhibitgoleftwhenx/=0[]λ：= 0reacts-toλ 0[]λ：=N对λ> N的端程序Unloader（j）在λ宣布z：整数最初z= 0时分配unload：：z：= 0ifz/= 0端组件购物车（2）[]加载器（1）在0 []卸载器（1）在NProgramLoader（i）at λ宣布y：整数最初y= 0时分配load：：y：= y。（y >0）如果y= 0端JJ1互动2推车（k）.x，装载机（i）.y：=装载机（i）.y， 0当Cart（k）.x= 0时Loader（i）.y/=0λ= 0[]Cart（k）.x，Unloader（j）.z：= 0，Cart（k）.x当Cart（k）.x/=0时卸载器（j）.z= 0Cart（k）.λ=N末端行李传送器264C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276然后向左简单地更新车在赛道上的位置。当购物车为空时，第一个初始化语句阻止执行go right语句。类似地，另一个inhibit语句防止推车在非空时向左移动。剩下的两个语句是反应状态。第一个是启用时，车是在一个位置小于0。如果在程序中执行正常语句后，该语句变为启用状态，则推车的位置将更新为轨道上的合法位置（位置0）。类似地，第二个反应语句在启用时将强制推车到达轨道上的合法位置，即位置N。系统中剩下的两个程序，Loader（i）和Unloader（j）是简单的程序，每个程序都包含一个赋值语句。在Loader（i）中，准备将一个值装载到推车上;在Unloader（j）中，从系统中删除一个值。当我们考虑这三个程序如何相互作用时，这两个程序的操作就更有趣了。MobileUNITY系统的组件部分定义了组成系统的程序及其初始位置。在本例中，系统包含两个推车（索引为推车（1）和推车（2））、一个装载机和一个卸载机。装载机和卸载机具有指定的初始位置，而推车的初始位置不受限制。Interactions部分允许推车、装载机和卸载机程序实例化一起工作以运输行李。第一个语句是异步值传输，条件是购物车的位置和loader的状态。由于所有的自由变量都被假设为是泛量化的，该语句描述了典型的装载器和典型的推车之间的关系，因此该语句适用于两个推车。存储在Loader（i）.y中的负载被转移到推车并存储在Cart（k）.x中。这使得推车能够开始朝向卸载机移动。 类似地，推车到达轨道的右侧使得负载能够从Cart（k）.x转移到Unloader（j）.z，稍后被丢弃，如在卸载器的代码中所示。由于禁止声明防止推车移动，因此确保推车与装载机或卸载机之间的转移。如[15]所示，许多不同的协调结构可以由到目前为止所介绍的基本结构。其中，一个特别感兴趣的是瞬态和传递变量共享，表示为。例如，下面的代码描述了购物车和检查员之间的交互，其中购物车和检查员共享变量y和w，就好像它们表示相同的变量一样。Cart（k）.y=Inspector（q）.w当Cart（k）.λ=Inspector（q）.λ时engageCart（k）.y脱离推车（k）。y，0在推车和检查员位于同一位置时，共享变量C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276265able是由engage子句指定的cart的y变量的值当cart和inspector不再位于同一位置时，cart除了上面描述的结构之外，Mobile UNITY还提供了在assign部分中使用的事务事务捕获一种顺序执行形式，其净效果是大粒度的原子状态更改（在没有反应语句的情况下）。事务由一系列赋值语句组成，这些语句必须按照指定的顺序进行调度，并且没有其他语句交错。交易的符号为：标签：：s 1; s 2;. ;sn上面描述的反应式语句可以与事务中的语句交叉。inhibit构造还可以用于保护事务的执行。Mobile UNITY霍尔三倍。这种差异是由于抑制性陈述和反应性陈述的引入造成的。例如，在UNITY中，属性如下：{p}s{q}其中s在P指的是一个标准的条件多重赋值语句s，与它在程序P的文本中出现的完全一样。相比之下，在Mobile UNITY程序中，需要使用：用途：∗{p}s{q}，其中s ∈ q，其中，表示P的正常陈述，而s表示被修改以反映由抑制状态引起的防护加强的正常状态s在由P中的所有反应语句组成的反应程序结构中，反应语句的执行所导致的扩展行为。下面的推理规则捕获了与在Mobile UNITY中验证Hoare三元组相关的证明义务，假设s不是一个事务：p<$i（s）<$q，{p<$i（s）}s{H}，H<$<$→（FP（s）<$q），单位：{p}s{q}对于每个非反应语句s，i（s）被定义为命名语句s的抑制子句的所有when谓词的析取。 因此，假设的第一部分指出，如果s在满足p的状态下被抑制，则q对那个状态也必须是真的。{pi（s）}s{H}（来自假设）被认为是非增广陈述s的标准霍尔三元组。H是在s未被禁止的状态下执行s之后保持的谓词。 在反应式程序中，要求H指向固定点，q指向固定点。为一个事务验证Hoare三元组需要另一个推理规则[23]这里为了简洁而省略。266C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-2764形式化如前所述，这项工作的目标是使移动性的正式模型适应上下文感知环境，以允许推理程序，使其行为适应不断变化的上下文。考虑到我们正在使Mobile UNITY适应上下文感知环境，我们可以使用的工具在本节中，我们通过使用一个详细的例子来介绍在Context UNITY中表达上下文感知系统的符号的细节。在讨论了基本程序和符号之后，我们通过示例程序的扩展讨论了非确定性赋值语句在定义上下文中的作用然后，我们提出了定义程序与其上下文之间关系的选项。最后，我们讨论了如何上下文UNITY程序可以减少到移动UNITY。4.1一个简单的上下文UNITY示例图3中给出了一个示例ContextUNITY系统。推车程序文本指定了对原始推车程序的修改，以便推车根据其上下文调整其运动。 该推车感测其是否应该被装载或卸载，并且作为响应在装载机的方向上行进或卸载器。与前面的示例不同，推车不需要预先知道装载机和卸载机的位置，甚至不需要知道它们所处的方向为了保持示例的简单性，并将重点放在上下文的合并上，这个程序只允许使用一个cart、loader和unloader。我们稍后讨论一个更复杂的程序，它允许每个程序的多个实例化。该系统最新颖的部分是Cart程序对其上下文的定义。在这个讨论中，我们主要从购物车的角度进行讨论购物车是我们的参考程序。我们系统中的另外两个程序，Loader和Unloader，是被动实体，只使用本地信息。Cart程序在declare部分定义变量x、d、l和u与第3节所述的MobileUNITY系统一样，x是代表推车当前负载的变量我们将x称为局部变量，因为在cart程序之外没有使用该变量其余变量d、l和u在Context UNITY中被称为上下文变量，因为它们直接建模、访问和修改程序中的上下文。在购物车程序中，d用于表示购物车的目的地。l是表示在装载机处可用的负载的上下文变量，并且u表示在卸载机处用于推车的货物的空间C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276267系统行李转移程序Cartat λ宣布x，d，l，u：integer，[：integer]alwayschanged（l）=[（l/=initiallyx=0[][x<$=0]分配inc：：λ：=λ+1[]dec：：λ：=λ−1[]当d≤λ时抑制inc[]当d≥λ时抑制dec[]load：：x，l：=l，0ifl/n=[<$l：=lifl/[]unload：：x，u：=0，x，ifu/u=[u<$：=uifu/上下文定义d：=Loader.λwhenx=0 <$Loader.y/= 0∼Unl oader. λ，当xi=100时，z=0时[]l：=Loader. ywhenLoader. λ=dλLoader。y/=0d=λx=0[]u：=Unloader.zwhenUnloader .λ=d<$Unloader .z= 0<$d=λ<$x/= 0解决加载器.y：=lreacts-tochanged（l）响应l= 0[<$l：=lreacts-totochangeed（l）<$l=0][]Unloader.z：=ureacts-tochanged（u）u/=0[u<$：=ureacts-tochangeed（u）端程序加载器在λ声明y：integer初始y= 0指定载荷：：y：= y J。（yJ>0）ify= 0端程序卸载器在λ声明z：integer初始z= 0指定unload：：z：= 0ifz/=0端组件推车[]装载机[]卸载机结束行李转移图三. 示例上下文UNITY系统268C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276Cart程序定义了两个附加的变量，你，我称 为 影 子 变 量 。 在 图 3 所 示 的 系 统 中 ， 程 序 显式地确保语句 包含l 的l_a_t_k_n_v_lue，以便触发希望响应l中的更改的语句。同样的道理也适用于他有一个可供选择的人。这是一个阴影，所以variable是包括在他的为了清楚起见，我们使用了一个示例程序，但是上下文UNITY假设这些变量是标准的，除非需要显式更改，否则程序员不需要处理它们。当程序使用依赖于shadow变量的更改后的宏时，在图3所示的程序的resolve我们强调使用阴影变量，具有q个块的程序，例如， [（l/=<$l）]。在一个角落里，UNITY程序中，分配给这些影子变量的语句将不可见。cart程序的initial部分可用于在执行开始时为变量提供初始cart的initial部分用于声明cart在执行开始时是空的assign和context部分强调了上下文UNITY中上下文的使用。局部变量和上下文变量用于赋值部分以实现程序的目标。语句inc和dec通过简单地赋值给可分辨变量λ来更新购物车的位置。两个禁止语句用于防止不必要的推车移动。正如第3节中详细解释的那样，这些抑制语句加强了对inc和dec语句的保护，防止它们在某些条件下执行。第一个禁止语句防止推车在已经到达目的地（d）时向右移动，或者在目的地向左移动。第二个防止推车在推车处于其目的地或应该向右移动以到达其目的地时向左移动。目的地d的值由上下文确定。我们稍后将更详细地讨论它的价值。当执行load语句时，负载l从加载器中取出，并通过赋值给x放入cart中。同时，推车需要一个机构来向装载机指示它已经装载了货物。Cart程序通过对l进行局部赋值，然后将值l赋值给加载程序前者是程序代码的一部分，而后者则表示为上下文操作的一部分。我们将这种响应于程序状态变化的上下文更新称为项目关系，它捕获了上下文的局部操作导致新值被投影到系统配置上的概念。这个投影是由上下文部分中的一个规则定义的，下面讨论。最后，结合负载的移动，Cart程序显式地更新C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276269这将最终触发先前的操作返回到加载器。unload语句以类似的方式工作load和unload语句都以两种方式利用程序首先，这些语句使用变量l和u中的上下文反射来确定推车是否应该被装载或卸载，并将负载转移到推车或卸载机上。在上下文变量的当前值中的上下文的反射由反射关系捕获，该反射关系在这里被指定为对程序的上下文部分中的上下文变量的赋值。第二，load和unload语句通过对上下文变量l和u的赋值将更改投射到全局上下文上。如前所述，项目关系也在程序的上下文部分中指定。程序的上下文在上下文部分中定义一般来说，程序的上下文可以包含整个网络中可用的任何信息。 在程序和变量的Mobile UNITY术语中，系统的这种全局状态包括系统中所有程序定义的所有变量。在然而，事实上，程序希望保持它们的一些数据的私密性。 因此，我们引入术语暴露变量来指代程序中被其他上下文使用的变量。系统中程序的最大上下文是所有程序中所有暴露变量的联合;我们将其称为系统配置。在实际的程序定义中，暴露变量看起来和其他变量一样;这个术语只是提供了讨论上下文定义的必要语言。系统配置由上下文变量反映的方式在上下文描述的定义部分中指定。简单地说，程序中用于捕获其上下文的变量是基于当前系统配置定义的。 随着配置的变化，上下文变量的值也改变以反映当前环境。在cart程序中，上下文的反射由上下文变量d、l和u定义。推车的目的地d被定义为推车应被装载时装载机的位置，即，当购物车为空时（x= 0）并且加载器具有可用的加载（Loader.y/= 0）。当推车需要卸载并且卸载机有可用空间时，定义目的地d卸货机的位置上下文变量l的更复杂的反射关系如下：l：=Loader. ywhenLoader. λ=dλLoader。y/=0d=λx=0when子句的使用确保了当选择执行此语句时，只有在满足列出的四个条件时，才会分配loadl。第一个条件是加载器的位置Loader. λ相同作为目的地D。第二个状态是装载机有一个负载要给出270C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276推车，即，加载器y/= 0。 第三个条件是购物车是空的（x= 0）。最后一个条件d=λ，表示购物车位于上下文变量d指定的目的地。当所有这些条件都成立时，空推车位于所选的非空装载机处，并且推车将给定负载（l：=Loader.y）。上下文变量u的反射关系以类似的方式指定：u表示放置负载的空间，并且仅当非空推车出现在所选的空卸载器时才定义。程序变量由context的resolve部分指定。每次更新购物车通过使用函数changed，在购物车的resolve部分捕获此条件resolve部分中的第一条语句将加载cart的效果投射到上下文上：Loader.y：=lwhenchanged（l）l= 0[<$l：=lreacts-totochangeed（l）<$l=0]程序对上下文的影响的定义是一种反应状态，并在执行任何语句后立即进行评估。这种投射上下文的反应式定义确保加载器知道它的加载一发生就被拾取了。根据这个定义，每次执行cart程序中的语句，导致cart不是空的并且cart的负载l已经改变的状态时上下文变量l被投影到加载器的变量Loader.y中加载器处的可用负载）。由于当cart将其本地loadx更改为非零值时，它在assign部分中将l设置为零，因此投射到Loader.y的值将为零。类似的对于卸载器发生上下文的反馈：当推车在分配部分中放下一个负载时，上下文变量u被设置为负载x的值。4.2语境定义上面用来展示Context UNITY的基本概念的示例程序在程序中使用了一个相对简单的上下文定义，其中系统的整个状态总是已知的。只有当人们检查可以使用该模型表达的复杂上下文时，才能充分认识到上下文统一性的力量。接下来，我们讨论使用非确定性赋值语句来提供更专门的上下文反射和投影。然后，我们添加了量化的概念，以扩展上下文统一的上下文定义的力量非确定性分配。在上下文UNITY中，使用非确定性赋值语句被证明是提供可解释的上下文定义的必要条件。这一点在之前提出的简单例子中并不明显C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276271上下文定义d：= dJ. （j，y：！Loader（j）加载器（j）.y/=0：：dJ=Loader（j）.λ）当x= 0时J.（j，z：！卸载器（j）卸载器（j）.z = 0：：dJ=卸载器（j）.λ），当x/=0时[]l，i：=（l J，i J）。（j，y：！Loader（j）Loader（j）.λ=dLoader（j）.y/=0：：lJ，iJ=Loader（j）.y，j）当d=λx= 0[]u，i：=（uJ，i J）. （j，z：！卸载器（j）<$卸载器（j）.λ=d<$卸载器（j）.z/=0：：uJ，iJ=Unloader（j）.z，j）当d=λx/=0解决Loader（i）.y：=lreacts-tochanged（l）l= 0[<$l：=lreacts-totochangeed（l）<$l=0][]Unloader（i）.z：=ureacts-tochanged（u）u/=0[u<$：=ureacts-tochangeed（u）见图4。非确定性语境定义因为系统本身就是决定性的。然而，如果推车被放置在它没有信息的环境中，它应该能够利用其任务的知识来发现关于其上下文的所需信息。通过使用非确定性赋值语句来定义其上下文，程序可以从满足某些条件的一组值中为其上下文变量选择值。例如，在我们的程序中，如果为空，它需要找到任何负载y/= 0的加载器。 如果这样的程序如果找到，则推车应开始向装载机的目的地移动。这允许系统包含多个加载器，如在原始Mobile UNITY 程序中那样由整数索引（例如，Loader（i）是指第i个Loader）。这个修改后的cart程序的上下文部分如图4所示。的符号！Loader（i）用于表示第i个名为Loader的存在.在上下文定义中，cart现在使用非确定性赋值语句来定义其目的地d，该语句基于相应组件必须满足的属性来选择加载器或卸载器。例如，在第一种情况下，购物车是空的（x= 0），它正在寻找一个装载机，一个加载到操作器（Loader（i）.y0）。任何符合此规格的装载机将请稍等。如果任何装载机满足条件列表，则非确定性地选择一个装载机以类似的方式选择卸载器。一旦到达目的地，上下文变量l或u也相应地更新。在加载动作的情况下，一个关键的添加是使用了一个新的上下文变量i，它用于准确地记住推车从哪个加载器加载。此信息由resolve节以确定性的方式用于更新相应的加载程序。在选择装载到推车中的负载时，上下文定义非确定性地选择在目的地位置处具有负载的装载机（多个装载机可能在相同位置处）。所选加载器的加载和标识的值存储在上下文变量l和i中。再一次，272C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276u的定义类似于l。resolve部分中的唯一更改确保了cart从中进行加载的加载器与更改投射回的加载器相同。非确定性赋值语句也可以在上下文的resolve部分中使用，以将更改投射到非确定性选择的变量上。虽然在我们的示例程序中不会立即有用，但我们可以想象多个卸载器位于同一位置的情况。上下文变量u可能实际上反映了一个特定的卸载器，但在投影阶段，购物车只需要确保它卸载到位置d处的卸载器上，而没有当前的负载。卸载程序的解析规则示例可能是：J⟨ǁ j：j = j. （！卸载器（j）<$卸载器（j）.λ = d <$卸载器（j）.z = 0）：：Unloader（j）.z：=u这非确定性地选择满足条件的单个卸载器，并将其变量z设置为卸载的负载。量化。在程序上下文的定义中使用非确定性分配状态的关键是它们能够扩展定义能力。例如，cart程序不仅可以从一组加载器或卸载器中选择任何组件，它还可以选择最接近的组件，组件或加载程序中的最大负载。在这两种情况下，只有上下文变量d的定义发生了变化，而上下文部分的其余部分保持不变。这也证明了上下文变量定义的模块性图5显示了移动到最近的装载机或卸载机时d的重新定义。 我们使用符号D来表示距离公式，即， D（λ1）= |λ1−推车λ|。从这些例子中，我们Jd：= d。（j，y：！Loader（j）j=mink：Loader（k）. yi=0D：：（Loader（k）.λ）J：：d=Loader（j）.λ）当x= 0时J很好。（j，z：！卸载器（j）j = mink：卸载器（k）.z = 0：：D（卸载器（k）.λ）J：：d=卸载器（j）.λ），当x/=0时图五. 查找最近的装载机和卸载机可以看到，使用非确定性赋值语句来定义上下文变量允许程序定义更灵活和表达性更强的上下文来进行操作。4.3上下文一致性上下文UNITY不仅提供了给出上下文的灵活和表达性规范的能力，而且还提供了指定系统配置和程序抽象之间C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276273上下文程序的上下文变量和可用的全局上下文之间的关系正如名字所暗示的那样，急切关系在程序和上下文之间强制执行高级别的一致性，而懒惰关系具有较弱的语义。为了充分解释渴望和懒惰关系的语义，值得注意的是关系类型是如何具体化和实现的。急切的关系是用反应性陈述来具体说明的。每次选择和执行程序中的任何语句时，都会评估反应语句。当在上下文定义或解析语句中使用反应语句时，结果是程序上下文变量和系统配置之间的高度一致性。 条件赋值语句，when子句用于指定惰性关系。这些陈述是非确定性选择的。如果语句被选中并且满足when子句施加的条件，则执行该语句。这导致了较弱的一致性水平，因为条件赋值是se-在执行中的任意点选择，但在有限的经常。因此，通过在上下文解析部分使用懒惰语句，可能不是程序状态中的每个更改都将被投射到系统配置上。同样地，并不是系统配置的每一个变化都将在上下文定义部分中使用惰性赋值语句在上下文变量值中反映出来4.4上下文UNITY和移动UNITY值得注意的是，我们的上下文UNITY计划中缺少了MobileUNITY的交互部分。在Context UNITY中，程序之间的大多数交互都是通过新引入的上下文部分定义的。这是由于上下文感知计算的一个关键方面：对基于程序的独特性来呈现上下文的非对称上下文的定义的期望。环境的视角。Interactions部分可能仍然存在于Context UNITY程序中，但它在这种情况下的使用超出了本文的范围。本文中介绍的上下文UNITY中的所有结构都可以通过使用交互部分在Mobile UNITY中复制。本质上，系统中所有程序的上下文定义和解析语句都可以稍微修改并包含在Mobile UNITYInteractions部分中，从而完成与Context UNITY系统相同的任务。因为Context UNITY直接简化为Mobile UNITY，所以我们可以完全重用Mobile UNITY然而，上下文UNITY带来了一种为上下文感知计算量身定制的表示法，它所提供的表示法更自然地适用于系统的表示，274C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276目的是向在由许多异构的动态程序组成的环境中操作的单个程序呈现上下文信息。5讨论上一节中讨论的模型强调了形式化上下文感知计算所必需的基本概念在上下文感知系统领域，该模型可以用来描述已经在应用程序和系统中实现的许多组件。例如，上下文变量可以以这样一种方式进行结构化，即它们表示由系统的某些部分中可用的数据定义的一个GUID数据结构。几个移动计算系统[8，14，19]使用这种数据结构查看系统中可用的数据。私有变量和公开变量之间的区别甚至可以允许对需要安全通信的上下文感知程序进行推理。本文提出的上下文UNITY代表了在移动环境中引入一种新的上下文感知计算模型。在我们的示例程序中，用于表达上下文定义和解决方案的符号虽然很有表现力，但有时可能看起来很复杂，难以阅读。对上下文统一性模型的进一步改进将包括简化该表示法的构造;例如，模型中将包括对变量进行阴影以能够对其变化状态做出反应的需求。本文中给出了完整的符号，以完整而清晰地描述建模上下文感知所第4节还定义了一些用于反射上下文和投影到上下文的一致性语义，特别是渴望和懒惰的传输语义。探索这两种关系的其他可能的语义可以为程序员提供更多的灵活性和对定义和使用其定义的上下文的控制。当我们将这些和其他改进纳入模型时，我们将探索继承的MobileUNITY证明逻辑的正确性。我们将继续评估我们对Mobile UNITY的添加的减少;一些更改可能会导致对证明逻辑的必要修改对证明逻辑的评估，上下文UNITY程序中进一步应用场景的表达，以及上面讨论的改进都将反馈到评估我们模型的完整性和表达性。6结论本文介绍了Context UNITY的基础知识，这是构建用于上下文感知计算的显式推理的正式模型的第一步为了呈现模型C. Julien等/ Electronic Notes in Theoretical Computer Science 97（2004）259-276275这样就可以解释上下文统一和移动统一之间的关键符号差异。上下文统一模型引入了特定形式化上下文感知关键方面所需的结构，包括与由连接组件定义的上下文交互的能力，以及定义个性化上下文的能力，专门针对特定程序一个有趣的观察是，大多数复杂性都在于程序与上下文交互的定义和操作。这确实与我们的研究目标一致，简化上下文感知应用程序的开发。对模型的这种初步探索突出了对上下文感知特定构造的需求，并且由此产生的表达性上下文UNITY在为上下文感知计算提供完整的形式化模型方面表现出很大的希望。致谢本研究得到了美国国家科学基金会的部分资助。CCR-9970939和海军研究办公室MURI研究合同号N 00014 -02-1-0715。本文中表达的任何意见，发现，结论或建议都是作者的观点，不一定反映国家科学基金会或海军研究办公室的观点。引用[1] Abowd，G.，C. Atkeson，J. Hong，S.隆河，西-地Kooper和M. Pinkerton，Cyberguide：Amobile context-aware tour guide，ACM Wireless Networks3（1997），pp. 421-433[2] 回来，河。J. R.和K. Sere，St
我的内容管理
展开
