普适系统中的交互体验与性能建模

理论计算机科学电子笔记261（2010）23-42www.elsevier.com/locate/entcs普适系统中的交互体验、功能和性能建模Michael D. Mieke Massinkba英国纽卡斯尔大学计算科学学院b信息科学技术研究所。Faedo’, CNR Area Moruzzi 1，比萨，意大利摘要部署一个无处不在的系统来增强物理环境的成本可能是相当可观的。其部署的成功在很大程度上取决于其背景：物质环境和将在其中开展的活动本文提供了一个初步的探索是否随机过程代数（特别是PEPA与流体流语义）可能会被用来探索部署前的后果。探索的重点是帮助理解拟议的系统如何支持环境中的用户面临的挑战是提供符号和技术，使潜在的复杂系统的分析。关键词：交互系统，模型检测，随机建模，普适计算，人机交互1引言本文的出发点是这样一个概念，即普适系统可以被有意地设计来促进或修改人们在物理环境中的集体行为。因此，它假定设计人员将需要技术，使他们能够预测的影响，设计对那些人的互动系统内，使这种行为。 在人机交互交互式系统分析技术的传统焦点是用户和设备。这些技术中典型的是认知演练（[7]提供了对它和其他技术的描述），它评估了交互式设备支持典型的用户行为：他们的目标、他们实现目标的计划、动作的可用性以及动作效果的清晰度。本文简要探讨了可能需要更广泛的性质，使一个1电子邮件：michael. ncl.ac.uk1571-0661 © 2010 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.01.00424M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）23从用户的角度来看，无处不在的系统有效性和随机建模可能在这方面发挥构成无处不在的系统的技术的可用性和复原力的增加，为创造技术上得到加强的支持一系列活动的物理环境提供了机会。潜在的例子包括医院门诊病人，其中系统的作用是在咨询的每个阶段指导和告知病人，或者机场，其中航空公司向乘客提供关于登机牌的信息，机场当局提供与建筑和安全有关的服务，零售商提供关于食品、免税等的信息。如果这种环境要成功和适当，许多因素都是重要的。这些因素中的一些可以使用交互设计的传统技术来识别和构建到设计中，例如与单个设备或显示器的可用性相关的技术。这些技术涉及通过使用场景或任务来分析典型行为[21]。然而，无处不在的环境为可用性分析提供了额外的挑战。它们使用传感器来识别个体（使用感测标签或启用蓝牙的移动设备）并使用其上下文（例如，位置、目的地、先前行为、任务、意图）来定制提供给个体设备或公共显示器的信息。 它们通过推理隐含地支持活动一个人的环境变化，预测他们的需求。 诸如这些的特征具有使用户沉浸在系统内的效果，使得有可能在技术增强的环境中为用户创建或设计体验。系统可能采取的隐式操作将取决于许多因素，例如，该个体是否具有移动终端、其特征是什么、以及还有谁在该空间中。例如，MATCH系统[17]旨在为有特殊需要的人提供辅助生活。当检测到潜在不良事件时，系统根据上下文采取多项措施。如果看护者与个人在同一个房间，那么系统什么也不做。 如果看护人在同一所房子里，但不在房间里，那么看护人也会被提醒。通过声音或通过移动终端上的消息，取决于环境条件 在他们所在的房间。如果照料者不在同一所房子里，则通知庇护所的监督中心传统形式的可用性分析不足以分析这些系统的经验，他们创造。需要补充技术，侧重于享受、安全或保障意识或在物质环境中提供位置感等问题。这些补充技术已经在更广泛的设计社区中受到关注，如[1]所讨论的。激励本文的问题是如何理解和设计的经验，什么样的作用，如果有的话，一般的建模技术和随机建模技术，特别是将在该分析。环境设计的许多特征可能会对体验产生影响（享受，挫折等）。环境的使用者。请考虑以下示例：到体育馆或体育场观看足球比赛的游客M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）2325将需要有关如何到达指定位置或体育场内座位的信息。根据个人需要及时提供相关信息，使游客能够顺利抵达目的地，不会感到困惑或沮丧。疏散办公楼或体育场的人们：在他们离开的每个阶段都需要清晰和冷静的指示，以确保他们采取最佳路线，避免拥堵。航空公司的乘客：将需要通知他们在办理登机手续、行李检查、护照检查等时应加入哪个队列。在每个阶段单独提供的关于对他们的期望的信息可以减少等待，并提高机场作为一个地方而不是一个令人生畏的空间的感觉医院门诊病人：将需要根据其预约的性质和他们已经达到的阶段的指示，进行血液检查，或X光检查，或者扫描，或者看医生，或者参加健康检查。新注册的大学生：在课程开始时，作为注册过程的一部分，需要指导他们获得图书证，支付费用，见导师这些系统的体验也可以通过一些技术来改善，以处理空闲时间，例如在体育场或机场，可以在活动/登机前向游客提供有关零售或娱乐机会的建议，以填补空闲时间。如果医院门诊病人正在等待和符合资格，并且有多余的能力提供这些检查，他们可能会被告知常规检查的可用性。一个模型，只旨在捕捉这些无处不在的系统的功能特性可能不足以解决所讨论的经验要求。增强环境的纹理和物理特性，以及系统的普遍环境背景，对于在其中的体验是至关重要的。如果这些要求要表达一个新的设计，那么一个重要的问题是如何为实现者表达这些要求，以便他们可以在设计中放电。关于经验要求的文献（例如，见[1]）提出了建立和表达要求的若干阶段。第一个阶段是如何获得信息，了解什么会创造或破坏一种期望的体验。 这可以通过从典型用户（或特定类型的用户）获得叙述或场景来实现，其中现有系统已经创建了负面体验或发生了积极或期望的事情。情景可能是对最近糟糕经历的描述，例如，关于延误的航班，几乎没有提供关于延误程度的信息，或者是否有替代航班，排长队，没有考虑乘客在下一个机场的转机时间。 场景可以是一个新设计的发电机，有助于避免所描述的sce- nario的陷阱。另一种补充方法是要求个人在进行活动时记录他们的经历（使用录音或制作照片，并附有评论以解释记录信息的重要性）。在现有的系统中。这个过程的第二个阶段是在设计中有效地使用信息26M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）23叙述可以用来探索一种新的设计选择。 可以构建修订的叙述，其中包括如何使用设想的设计的描述。这些叙述可用于与潜在用户探讨新设计会是什么样子，使他们能够可视化其影响。 这种可视化类似于在更广泛的设计社区中常见的过程，例如，粘土模型代表一个提案，并由主题在日常活动中使用或可视化[1]。 导出的信息该过程的第一阶段还可以包括对设计的期望特性的理解。这些特性可能与信息显示器相对于房间中座位的位置有关，可能与在过程的哪个阶段需要什么信息有关，可能与延迟的可接受性或其他有关，以及定期更新信息的必要性有关。在这里，功能模型将能够描述这些关系，表示为属性，提供分析的基础。该模型的结果可以作为性质突变的反例。这些反例可以被动画化，从而可视化，以生成与所提议的新设计相关的进一步场景供考虑。本文重点讨论了与开发一类无处不在的系统的功能模型相关的挑战，这些系统的设计可能受益于定性和定量推理。本文首先描述了一类可能对这种分析敏感的系统（第3节）。它通过两个例子演示了类。虽然这些系统的各种属性可能与用户对这些环境的体验有关2相关工作在该文件中采取的方法是关注使用的形式化建模和相关的分析技术的无处不在的系统的交互方面。已经有大量的文献中的作用，形式化方法的设计和评估的交互式系统。当前形式分析的大部分焦点都是基于模型检查或其他算法技术，例如图分析。分析的一个动机是发现可能存在问题的行为实例，然后由人为因素和领域专家进行分析领域专家根据分析结果生成系统工作的更丰富的描述，人为因素专家根据痕迹探索感兴趣的典型属性包括可预测性、可见性、恢复到先前状态的能力和模式结构的清晰度模型专注于系统中交互的关键特征，使用诸如模态动作逻辑（MAL）[2]，状态图[6]或矩阵[9]等符号对飞行管理系统[23，2]、车内控制系统[3]和医疗仪器[24]进行了建模和分析，在每种情况下都预测了设计的不可预见后果进一步的符号与普适系统相关，以模拟整个环境。这意味着捕获：M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）2327• 环境的空间布局，建议定义移动性和空间的逻辑属性（例如，KLAIM和π演算[5，19]和环境演算[4]）• 访问者的属性，例如假设访问者的目标或定义错误行为，这里的相关研究探索了人类认知过程的模型，例如[22]• 可以用来进行隐式操作的上下文相关的研究还涉及到与普适系统相关的协议的形式化分析，例如[8]关于订阅订阅和[16]关于八卦协议。泛在系统中人类交互行为的特点需要 不仅要在功能上表达，而且要以一种形式来表达，这种形式使人们有可能探索空间中多个居住者的随机行为3例如：指导和门诊病人一类普遍存在的系统形成的基础上提出的定量分析的用户相关的属性。这类系统旨在通过为环境中的人提供指导信息来增强建筑物，并适用于一系列领域。 两个例子用来说明共性：引导系统和辅助医院门诊病人的系统3.1制导系统第一个系统引导不熟悉办公楼的游客到大楼的特定位置。 来访者唯一需要做的就是以某种方式确定它们的目的地例如，这可以通过访客的徽章或访客在他们的电话上的日记来完成。该系统使用一组固定在建筑物墙壁和门上的显示器。它的灵感来自于兰开斯特大学安装的现有系统[14]。 显示方向 在根据显示器附近的人想要的位置而改变的位置显示器（参见图1的走了取决于谁在场，显示器指示与他们相关的一个或多个方向。 这样的系统可以安装在博物馆、音乐会大厅或体育场，人们大量到达，通常不熟悉他们的座位或其他理想位置的位置几个人可以同时在一个特定的空间。出于这个原因，不止一个方向与其相关的目的地一起显示，以便访问者可以选择与他们相关的方向。由于集体行为受到关注，因此假设空间具有特定的容量。 在抵达有显示器的空间有四种可能性。(i) 与人的目的地相关的方向28M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）23Fig. 1.现场展示视情况而定）。(ii) 当前未显示相关方向，但公共显示器上有一个空槽。在这种情况下，自动下载指定目的地的相关方向（就访问者(iii) 不显示相关信息，并且没有空插槽。如果空间没有装满人（比如说已经有少于25人在等待），这个人将等待，定期阅读显示器，直到显示器最终更新为显示所需的目的地。(iv) 当没有空插槽时，目的地没有表示，并且空间的容量已经超过，人随机移动到另一个空间。3.2门诊系统第二个例子是为医院的门诊病人设计的。一个病人带着预约来了。 无处不在的系统的目的是为患者提供信息和指导，以便他们（1）保持与等待时间有关的最新信息（2）在患者行程的下一阶段被引导时，患者可以具有移动设备，在这种情况下，与他们相关的信息被直接发送到他们的设备，或者没有适当的移动设备，在这种情况下，他们被发放有传感器/访客卡，该传感器/访客卡可以由环境使用以识别他们接下来必须做什么。在后一种情况下，公共显示器会更新病人的号码和关于等待时间的信息或关于下一步去哪里的指导。一个简单的系统可以识别四种类型的病人：(i) 只需要看医生的病人（D）(ii) 需要X光检查的患者（X）然后去看医生（D）(iii) 需要验血（B）和看医生（D）的患者(iv) 在看医生之前需要验血（B）和X光（X）的患者（D）。此外，如果有可能在下一阶段的程序之前完成检查，则对某些类别的患者进行健康检查。相关信息将被发送到个人M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）2329EA B C D图二. 建筑布局如果他们没有移动终端，则他们占用该移动终端。系统将重新安排类型（iv）的患者，以便安排（B）和（X）中最可用的患者。 如果有时间，则进行健康检查（W）。3.3设计之间的共性这两个例子有共同的特点。它们涉及个人到达目的地。在一种情况下，一旦识别出访客的目的地，系统就确定到达目的地的路线，在另一种情况下，它取决于患者类型，所有患者的目标都是到达相同的目的地。因此，两者都适合于根据上下文推送信息的一般系统。在每种情况下，人们对信息的反应都是采取行动，以某种方式改变他们的环境4制导系统第一个例子将用于探索什么可能是普适系统的适当属性。正如已经讨论过的，与用户体验有关的许多属性取决于环境的特性，包括其纹理、知道接下来发生了什么、知道事物在哪里等等。体验通常与信息的传播速率和相关性有关 在系统中[18]以及当存在误解或错误时会发生什么。用户体验的一个重要特征是它是由上下文环境决定的。4.1性能在引导系统的情况下，访问者（其可以是患者）采取的唯一有意的动作是在事件之前的某个时间购买电子票，或在接待处获得访客通行证，或携带带标签的访客卡，或携带蓝牙功能的移动电话。否则，所有与系统的交互都是在访问者改变他们的环境时隐式发生的，例如从一个房间移动到另一个房间或从一个走廊移动到另一个走廊。环境的经验取决于这些信息。来访者或病人参与了一次旅行，无论是从到达门诊病人到咨询后离开的病人旅行，还是从接待处到办公楼目的地的来访者旅行。许多因素可能对环境中的人产生影响。它们的相关性取决于具体情况，并将通过某种形式的用户评价进行评估。这些因素可包括：30M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）23(i)显示方向的可见性和解释(ii)无论用户身在何处，(iii)朝着目的地前进的感觉(iv)记住完成一次的路线的能力(v)更广泛意义上的建筑物和它所拥有的设施(vi)在显示器与它们相关之前等待多长时间（根据显示器的刷新时间或次数(vii)保证到达(viii)如果许多用户需要恢复，(ix)一种拥挤的感觉，周围的空间里有太多的人所有这些因素都可能影响这些环境的用户的满意度或焦虑程度。然而，他们的体验也可能取决于外部因素和用户带来的期望。 其他无法在设计中建模的过程也会受到影响。 然而，只有认识到以及将系统设计与这些外部因素相关联的因素结合起来，从而取得进展。 虽然排在第一位的因素更熟悉，在可用性方面，从人机交互的角度来看，列表末尾的内容更加新颖。这些属性具有以下特征：• 它们是关于在需要的时间和地点提供相关信息，以及提供一种朝着目的地前进的感觉• 它们涉及如何使用特定的路线和指导来减少瓶颈的可能性。引导系统中的隐式交互可以通过将系统内的个人或一小群个人聚焦，或者通过集中于集体行为而从个人行为中抽象出来来建模。一个模型只有在具有形成价值时才有设计价值。它应允许探索设计方案的影响，并能够对各种方案进行比较。如果这可以在设计部署之前有效地完成，那么下游成本可能会 同时减少商誉这种分析虽然是技术性的，但应该以一种对那些关注人为因素方面的人有意义的形式呈现，并将模型所代表的设计5探索属性使用随机过程代数（如PEPA）的方法的优点[12]是有可能将捕获关键设计假设的功能模型与能够分析随机行为的技术相结合。这简化了在进一步的设计迭代中对结果的建设性使用。 将不详细描述PEPA。拟议的PEPA规范基于PROMELA [13]中描述的定性模型，该模型捕获了M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）2331系统[10]。 与定性模型相比的简化包括注重空间而不是位置。例如，访问者可能处于没有传感器或显示器的位置的可能性被忽略。该模型在规格是模块化的，由许多参数驱动一个专门构建的程序根据空间的组织，系统内的插槽，地点和个人的数量生成模型。该程序的输入描述了每个位置（1）它支持的位置数量， 显示器包含的插槽数量;（2）对于每个目的地，访问者的下一个位置。该文件还描述了在特定地点开始需要特定目的地的游客数量。 这些信息使得能够生成 一个适当的PEPA规范，它有一个形式，也使它适合到普通微分方程（ODE）分析[11]，建立在PEPA和相关分析工具的基于ODE的形式语义上[25]。为简明起见，本文中的插图仅限于五个位置。 两这些地方都是最终目的地。 这些位置被称为a、b、c、d和e，并以以下方式连接：（a，b）、（b，c）、（c，d）和（b，e），如图2所示。还分析了较大的配置，该方法已被证明是可行的建筑物与现实的位置和游客数量。该定量模型在其他方面反映了与[10]中描述的定性模型相同的结构和特征。每个位置都有一些地方，每个地方都有一些插槽，可供在场的游客咨询在位置上。显示器与传感器相结合，检测访客希望去哪里并显示相关信息。三种过程模型参观者的行为，展示和放置。PEPA模型由对访问者、仲裁员、插槽管理员、插槽和位置的行为进行建模的过程组成。插槽和位置为每个特定位置实例化。显示器由多个插槽组成。每个位置的插槽管理器和仲裁器确保显示所请求的信息，并且没有两个插槽显示相同的信息。访问者群体的定义是相同的起点和终点。例如，一个从位置a出发并首先前往位置d的访问者试图到达位置a中的一个地方，可以看到显示（LASD是试图获取位置A中的位置的动作）。 一旦一个地方已经获得了游客从事的行动laee到找出下一步该去哪里。只要有显示信息的可用显示槽，就执行请求。当信息显示时，访问者释放位置a中的位置（动作lasu）并接收信息(i.e.进程V中的任何匹配目的地是EdRec）。然后，访问者继续前进到所指示的下一个位置（例如，V是EdtoLb意味着具有最终目的地d的进入者现在首先需要前进到位置b）。到达最终目的地的过程由永远保持在状态V isEdArrived的过程来建模。PEPA中访问者进程的规范如下（参见[10]）：32M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）23××VisEytoLx=（lxsd，s）。（lxey，a）. （lxsu，s）. VisEyRecx VisEytoLy=（lesy，s）. （lyey，a）. （lysu，s）。VisEyRecx=（eexle，r）.VisEytoLe+（ eexla ， r ） .VisEytoLa+（ eexlb ，r ） 。 VisEytoLb+（ eexlc ， r ） 。VisEytoLc+（eexld ，r）。VisEytoLdVisEyArrived=（nop，a）. VisEy到达图三. PEPA的访客一般形式完整规格）。 在实际规范中，这些过程对位置的组合重复进行。访问者V的一般形式是EytoLx，当前在位置x，希望到达目的地y，如图3所示。访问者的模型有三个速率参数，模拟执行相关活动所需的平均时间。活动的平均持续时间按其速率界定，并假设以分钟计量。 例如，让s=10意味着访问者坐下或站起来所需的平均时间 是6秒。 (i.e. 0。1分钟）。 速率a=2表示访问者发出请求所需的平均时间为30秒。 速率r=1模拟接收的平均时间所请求的信息等于1分钟。还假设游客在一定时间内到达并前往不同的目的地。 这是以下列方式模拟的Vis=（nop，v0）。VisEetoLa+（nop，v1）。VisEdtoLa行动nop代表虚拟无操作行动。 速率v0和v1可用于调整两种类型的访问者（即前往e的访问者和前往d的访问者）的生成速率及其相对数量。 例如在 在总共60名访客的情况下，前往位置e的访客的数量，即，V是EetoLa过程的数量，将是v0/（v0+v 1） 60，而V是EdtoLa过程的数目总计为v1/（v0 +v 1）60。应该指出的是，这是一个模型的游客到达模式，其中大多数游客到达每个位置都使用一个仲裁程序，根据访问者的请求显示前往目的地的方向。仲裁器确保一个位置中的一个槽不显示同一位置中的另一个槽已经显示的信息。 进程ArbLaEe以空显示开始并等待请求从一个访客那里获取信息。如果这样的请求到达（laee），它会通过向插槽管理器进程（slaee）发送请求来设置一个插槽以显示所需的信息。然后，对相同信息的进一步请求不再由仲裁器处理，而是直接由相关槽处理。路由信息M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）2333SlotLa=（sslaee，100. 0）。（eealb，r）. SlotLadispEe+（Sslaed，100。0）。（edalb，r）. SlotLadispEdSlotLadispEd =（laed，a）. （edalb，rr）。SlotLadispEd+（freelad，f）. SlotLa SlotLadispEe =（laee，a）. （eealb，rr）。SlotLadispEe+（freelae，f）. SlotLa SlotLe=（sslee，100. 0）。SlotLe+（ssleed，100. 0）。（edelb，r）. SlotLedispEdSlotLedispEd =（leed，a）. （edelb，rr）。SlotLedispEd+（freeled，f）. SlotLe见图4。 位置a对于不同的目的地仍然由仲裁器处理，仲裁器将通过插槽管理器启动新的插槽，只要有可用的空插槽。插槽变为空闲，仲裁器通过插槽管理器（sfreelae）得到通知，并返回到其初始状态。仲裁员和插槽内部的活动被认为是相对较快的，这解释了所选择的固定速率100。ArbLxEy=（Ixey，a）。（slxey，100. 0）。（sfreelxy，第100页）0）。ArbLxEy如果一个位置只是一个最终目的地（因此没有其他目的地的游客通过这个位置），仲裁员不需要为个人设置一个显示槽：ArbLeEe=（leee，a）. ArbLeEe插槽管理器（SmanLxy）初始化并释放插槽。它接收来自该位置的仲裁器（slxey）的请求，以建立显示到特定目的地的路由信息的时隙。该请求之后是从插槽管理器到空闲插槽（sslxey）的初始化消息。插槽现在是空闲的通知插槽管理器（freelxy），然后转发到位置的仲裁器，该仲裁器跟踪空闲插槽和显示的信息（sfreelxy）。位于位置x的槽管理器处理对目的地的请求的过程。y是：SmanLxy=（slxey，100. 0）。（sslxey，第100页）0）。（freelxy，f）.（sfreelxy，第100页）0）。SmanLxy位置a的显示槽（图4）可设置为显示方向信息对于来自插槽管理器的消息之后的特定目的地，对于目的地d（sslaed）和目的地e（sslaee）。在为目的地d设置了插槽之后，该进程处理对该目的地d的请求。 当插槽已显示时则响应快得多，由速率RR给出。 信息可以通过由相关位置（x）和目的地（y）标记的称为freelxy的槽的自主动作从显示器移除它显示的信息。访问者是否可以看到显示器（即，a place is free）的模式如下：PlaceFreeLa=（lasd，s）. （lasu，s）. PlaceFreeLa34M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）23其中：（SmanLxy[1]Vis[400]）DL（SlotLx[2]ArbLxEy[1]PlaceFreeLx[100]）L=（请求-响应-ArbReqSlot-开始-ArbFreeSlot-释放-Slot-坐下-站立）请求={lXeY |X ∈ {a，b，c，d，e}，Y ∈ {a，c，e，d}}响应={eY XlZ|X，Z ∈ {a，b，c，d，e}，Y ∈ {a，c，e，d}，y/= x}ArbReqSlot ={slXeY|X∈ {a，b，c，d，e}，Y∈ {a，c，e，d}}ArbFreeSlot ={sfreelXY |X ∈ {a，b，c，d，e}，Y ∈ {a，c，e，d}}StartSlot ={sslXeY|X∈ {a，b，c，d，e}，Y∈ {a，c，e，d}}释放槽={freelXY |X ∈ {a，b，c，d，e}，Y ∈ {a，c，e，d}}Sitdo wn={lXsd|X∈{a，b，c，d，e}}Standup={lXsu|X∈{a，b，c，d，e}}图五. 系统的PEPA模型在分析的例子中，有四种类型的访问者。一种是从a开头的d，一种是从c开头的e，一种是从a开头的c，最后一种是从d开头的a。 总共有400名参观者，因此，对于v 0到v 3的指定速率，组分别由25、75、100和200组成。v0= 0。0625;v1 = 0。1875;v2 = 0。25;v3 = 0。5;Vis=（nop，v0）。VisEdtoLa+（nop，v1）.VisEetoLc+（nop，v2）。VisEctoLa+（nop，v3）。VisEatoLd整个系统由图5中的PEPA组成表达式给出。它由400名游客组成，分为四种不同的类型，每个位置有100个位置和2个插槽。这些进程在协作操作符列出的所有操作上同步。存在一个对本地显示进行建模的SlotManager，以及针对每个目的地y的每个位置x的一个仲裁器。6分析模型问题和挑战涉及使用该模型可以进行的分析类型，以及这些技术是否与前面部分讨论的属性相关。对于这个小例子，正在调整的设计参数包括显示器的设计，例如它应该同时包含多少个插槽。它将关注显示器的大小，有多少人可以同时看到它。它应该能够探索不同路径的使用以及这些路径如何消除系统的拥塞这将有助于设计M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）2335动态调度算法，旨在减少拥塞和等待时间。这些属性中的一些可以使用模型检查来探索，而其他属性可以通过模拟或基于微分方程的技术来探索。这里的问题是如何使用一系列技术来探索设计的这些经验要求。还需要做进一步的工作。以下分析实例是初步的，作为一项挑战而不是一组结果列入6.1PRISM分析PRISM [15]用于验证许多简单的定性和定量CSL特性。 这使得可信度检查，同时探索 模型假设的到达目的地的路径，以确保它们正确连接。例如，该分析用于检查进程的不同物质到达目的地d和e的概率，或者它们占据特定位置的概率。此外（对于模型检查案例中探索的有限数量的访问者实例），还探索了特定位置的作用作为多个路径中的一个步骤。 访问位置c的概率，为true，因为两个目的地都需要cP=？[trueU（PlaceFreeLc_STATE=PlaceFullLc）]//结果：0.996该模型用于确定访问者返回或不通过必要位置的概率。 它也被用来探索 访问者的两个不同实例都将在5个时间单位内到达目的地e和dP=？ [true U< =5（Vis_2_STATE=VisEeArrived&Vis_3_STATE=VisEdArrived）]//结果：0.0026523这些例子给出了随机模型检验可以发挥的作用的一个非常初步的指示。然而，可以看出，可以探索与用户在其中可能具有的体验相关的环境的一些特征。该分析使用更抽象的模型，与[10]中报告的定性模型检查所起的作用相似。然而，在目前的情况下，同样的模型可以用来验证集体行为。6.2基于随机模拟模拟和流体流动分析技术也可以使建设性的recruec- tion设计。这些技术将使用图2所示的建筑来说明，400名游客分为4组，从位置a，c和d进入，最终目的地为a，c，d和e。该模型已在上一节中描述。结果显示了10次独立重复的随机模拟，置信区间为0.05。另一个目的是说明两种技术之间的结果的对应关系，从而说明使用计算量较小的流体流动技术的价值。参数值汇总36M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）23率意义S=10平均而言，一位游客需要6秒钟才能坐到一个空座位上。一=1平均而言，访问者需要1分钟来请求信息R=2平均而言，一个插槽需要30秒来显示所需的信息RR=10平均而言，访问者需要6秒来阅读已经显示的指示F=0。2平均信息显示时间为5分钟表1参数值的定义模型的定义见表1。时间单位为分钟。图6（a）显示访客从进入建筑物的位置离开时在各个位置占用的位置数量 各自的目的地。第一个观察结果是，在位置d，最大数量的位置在一定时间内被占用（准确地说，大约100分钟，如相关曲线所示）。 在 其他地方几乎总是有足够的免费名额供游客使用。图6（b）所示的模拟结果与通过ODE获得的结果（图6（a））之间的对应关系表明，ODE结果具有预测性。显示0至300分钟时间间隔的结果图7（a）显示了游客到达各自目的地所需的时间。可以看出，50分钟后，所有最终目的地d的游客都到达了。请注意，到达时间还取决于这些访客进入建筑物的速度，而不仅仅是访客在每个位置花费的时间。上图显示，目的地d的游客总数为25人，e是75，c是100，而目的地a是200。图8（a）和图8（b）显示了不同位置显示器上的平均空槽数。最初，所有的插槽都是空的，但当游客到达这些位置时，它们很快就会被占用。当所有访客都到达他们的最终目的地并且显示屏上的信息被移除时，所有插槽都返回到空状态。即使有四个不同的目的地，显示器也最多占用两个插槽。在位置d中，最多只有一个插槽被占用，因为只有前往单个目的地的游客经过。 在位置e插槽仍然是免费的，因为它只是当前模式中的最终目的地，因此没有游客需要获得下一步去哪里的信息这些初步结果显示了一些希望。他们提供了洞察的影响，一个无处不在的系统设计对拥塞的用户在不同的交通情况。系统的设计可以根据显示器的大小（有多少人可以看到它）、显示器上的插槽数量以及为到达不同目的地而定义的路线的不同配置进行评估。这些变量可以被操纵。 例如，这种分析可以作为一种基础，用于在泛在系统内动态地改变路径以创建一种情况M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）23371008060402000 50 100 150 200 250 300以分钟为单位的(a) 随着时间的推移被占用的地方（ODE近似值）。1008060402000 50 100 150 200 250 300以分钟为单位的(b) 随着时间的推移，满座/座位的数量（随机模拟）。见图6。 对所占这将减少用户的沮丧或焦虑。将这些结果与系统的其他功能属性相结合，例如显示器的位置、信息发送的时间和地点、在显示器上看到个人目的地之前的典型延迟，将使人们能够更清楚地了解设计之前的情况。部署。本节的结果还表明，ODE技术可以处理大量前往不同目的地和从不同地点出发的游客位置满a位置满b位置满c位置满d位置满e位置满a位置满b位置满c位置满d位置满e种群规模人口规模38M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）232001501005000 50 100 150 200 250 300以分钟为单位的(a) 到达目的地的游客（ODE近似）。2001501005000 50 100 150 200 250 300以分钟为单位的(b) 到达a、c、d和e的游客数量（随机模拟）。见图7。来访者分析选项。这是因为它将访问者进程及其状态表示为连续量，而不是具有交错行为的大量离散实体。虽然模拟始终可以应用于PEPA规范，但如果需要高精度，则可能非常耗时。 这使得 ODE方法是模拟的一种有吸引力的替代方法，可以在早期设计阶段探索不同设计方案对游客流量的影响。用常微分方程得到的结果的可靠性可以很容易地（而且常常很快地）通过比较游客到达E游客抵达A来访者d来访者C游客到达E游客抵达A来访者d来访者C人口规模人口规模M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）233921.510.500 50 100 150 200 250 300以分钟为单位的(a) 每个位置显示器中的空闲插槽（约ODE）21.510.500 50 100 150 200 250 300以分钟为单位的(b) 随时间变化的空闲时隙数（随机模拟）图8。分析空闲插槽。结果与“有限的”模拟，其中只有几个独立的执行被认为是。如果存在合理的对应关系，则可以认为ODE结果具有充分的预测性。 如果没有合理的对应关系，那么，对于特定的分析，如果认为值得花费时间，那么总是可以在不改变模型的情况下Slots free in aSlots free in bSlots free in cSlots free in dSlots free in eSlots free in aSlots free in bSlots free in cSlots free in dSlots free in e人口规模人口规模40M.D. Harrison，M.Massink/Electronic Notes in Theoretical Computer Science 261（2010）237讨论和结论本文提出了两个发展方向人类互动工程技术的技术增强环境。第一个方向是更广泛地理解在这样的环境中可用性意味着什么。虽然需要更传统的可用性分析来评估设备和用户之间的交互，但需要进一步的技术来处理这些系统中发生的隐式交互以及人群系统交互的特定要求和关注点。通过明确交互需求，建模还可以为更清楚地定义特定系统背景下的“平静计算”[ 20 ]铺平道路下一步是在一个更大更复杂的项目中集成和使用本文中描述的方法。第二个方向解决的问题是，它通常是不可能的，以探索一个系统在其目标环境。 很难想象在这种情况下，拟议的设计会产生什么影响。 一个环境。与此同时，利益相关者将需要在商业或安全敏感环境（例如机场或事故和紧急情况）中引入新系统的强有力的理由，然后才能部署这样的系统。本文探讨了PEPA模型在分析多人智能环境中新颖的人性化方面所能做出的贡献。许多用户在同一时间移动通过同一空间并以隐式方式与其交互，并且在某些时间限制下，这提出了特殊的挑战。 如图所示，一种基于普通微分方程的方法--从对大型用户群和环境进行建模的过程代数规范中导出的TAL方程，有望为智能环境的集体行为的人类方面提供补充定量分析，这也可能在设计中形成。使用这种技术，不同的体积，速率和设计参数的假设可以比较迅速，适当的精度。技术增强物理环境的设计者是否会将投资于相对复杂和复杂的技术（与交互系统设计中经常使用的折扣可用性工程技术相比）视为使用它们的理由，这还有待观察。未来的研究需要降低这些成本，开发流程，属性模式和通用智能环境模型，使自动合成这些模型的任务成为可能，并方便开发人员。确认我们感谢Stephen Gilmore提供的有益建议，感谢欧盟抵抗卓越网络和意大利CNR项目XXL。