理论计算机科学电子笔记183（2007）3-20www.elsevier.com/locate/entcs模型检测驱动的交互系统设计Antonio Cerone1 和Norzima Elbegbayan2联合国大学中国澳门摘要本文介绍了一种基于模型检测的方法来检测系统的错误，通常由非专家用户。系统的人和计算机组件分别建模。 人类部分包括用户认知上合理行为的一般模型，然后可以将其细化为反映用户个性和技能相关方面的特定行为实例。我们认为，作为一个案例研究，一个正式的模型的在线互动工具，使会议与会者分享想法和反应，并选择匹配的与会者开始沟通。从最初的系统设计开始，使用模型检查技术来突出系统漏洞，这些漏洞来自与非专家用户的交互，并可能导致安全违规。分析的结果被用来改进设计，通过引入保护措施来减少甚至防止安全违规。关键词：形式验证，人类行为，可用性，用户错误，社会计算，过程演算，模型检查。1介绍计算机在安全关键系统和安全系统中的广泛使用增加了以减少人为错误的可能性的方式设计人机交互的需求。人的可靠性评估（HRA）技术，主要出现在20世纪80在20世纪90年代此外，运营商的行为往往1 电子邮件地址：antonio@iist.unu.edu2电子邮件地址：norzima@iist.unu.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.0584A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）3根据接口要求进行建模。然而，在现实中，与系统交互的用户在设计界面时并不一定表现得像预期的那样，错误实际上是通过交互出现的意外用户行为的结果为了最好地捕捉这种涌现行为，操作员的模型必须指定认知上合理的行为，即所有可能发生的行为，并且涉及不同的认知过程[1]。该模型必须考虑到用户的行为，用户的目标和环境之间的所有关系许多研究人员已经探索了使用正式的模型来理解认知错误如何影响用户的表现。Rushby [12]模拟了遵循警告显示灯的健忘操作员或没有警告灯的非健忘操作员的行为，并检查紧急模式混淆。Curzon和Blandford [5]专注于基于目标的交互，并对用户的行为进行建模，当目标实现时，假设所有任务都已完成，但忘记完成一些重要的附属任务（完成后错误）。在本文中，我们关注的是用于大群体的人，沟通，协作，信息交换和兴趣匹配的主要目标[8，9]。 在这种情况下，不存在安全问题，但系统必须易于使用，具有可学习性和效率，并保证法律和社区政策所要求的保密性和其他安全属性。界面的复杂性对于任何水平的用户来说都是可以接受的，系统不应因其操作性不足或不方便而使用户望而却步。此外，对用户使用该系统的行为和经验以及更一般的用户使用计算机和互联网的技能，也缺乏先验因此，重要的是要设定最悲观的情景，在这种情景中，用户不是专家，技能最少，并探索与各种态度和个性相对应的替代用户行为。模式混淆和完成后错误必须被认为是非常可能发生的。另一方面，系统的设计必须通过在交互的各个阶段提供适当的选项来指导用户我们使用在以前的工作中开发的建模技术[2]，这些技术基于CSP进程代数[10]和时序逻辑，首先将用户的目标和接口定义分析是通过指定时态逻辑中的属性并使用新世纪并发性检查器（CWB-NC）[ 4 ]模型检查器来验证模型的属性来进行的我们通过一个简单的案例研究来说明这种方法，该案例研究基于一个基于网络的在线互动工具，使会议与会者能够交流和分享他们对共享事件的想法和反应[7]。第2节介绍了一个可能发生在研讨会或会议期间的场景，在这个场景中，与会者通过一个由各种目标驱动的Web界面分享想法和意见（第2.1节）。我们还假设通过登录机制访问的Web界面的基本结构（第2.2节）。第3节简要介绍了本文中使用的CSP符号，A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）35根据三个可能的目标描述了用户行为模型，这些目标可能激励和引导用户与系统交互：在论坛中表达自己的想法（第3.1节），与匹配用户建立联系（第3.2节）以及收集有关其他用户的信息（第3.3节）。第4节提出了一个系统的初始设计，作为两个CSP过程（第4.3节）的并行组合，一个建模的用户权限（第4.1节）和其他建模的网页（第4.2节）。第5节确定了可能的安全威胁（第5.1节），定义了旨在防止安全违规的安全属性（第5.2节），介绍了对典型用户的专业知识和健忘性的假设（第5.3节），展示了如何在给定的安全属性假设下分析系统设计（第5.4节），并描述了设计的可能改进，以减少（第5.5节）甚至完全克服（第5.6节）初始设计的漏洞。2案例研究：会议系统这个工具包括一个基于网络的界面，它可以是一个更大的系统的一部分通过网页，用户收集有关会议（或其他活动）的信息，并找到/联系可能符合其兴趣的其他用户。然而，该工具不提供约会服务[9]。匹配决策由用户明确做出2.1场景我们开始考虑一个可能发生在研讨会或会议上的常见场景我们使用“用户”这个词来标识场景的主要主题在讲座或演讲之后，用户想要会见其他出席者以讨论对出席的演示的印象或这些与会者可能正在从事与我们的用户类似的项目，或者对演示文稿的主题有类似的想法。一个讲座通常涉及大量的与会者和每一个单独的与会者可以有不同的意见关于这个话题。在系列讲座中，与会者没有太多机会相互交流和征求意见。因此，重要的是允许用户在参加会议之前搜索和发起通信，以便在会议期间提前计划和预约要举行的一个会议有一个网站，专门用于分享和讨论有关讲座和研讨会的想法和建议。在这样的网站上，用户可以设置自己的个人资料，并浏览其他用户该系统的目的是帮助人们见面并分享他们对讲座或其他活动的意见和反应，这些讲座或活动将（或已经）在会议期间举行。会议网站包含会议的所有信息，包括讲座和活动的我们假设用户已经开始分享他们的6A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）3在会议开始前的想法和意见。在一个典型的情况下，用户访问网站，浏览事件和讲座的列表，阅读讲座笔记和论文和演讲的摘要。登录后，用户可以设置个人资料，其中包括选择一些关键字来代表用户用户还可以：阅读其他用户发布的消息，以了解其他人发布消息以分享对最近事件/演示的想法和意见;回复其他用户发布的消息，以支持或试图反驳他们的想法和观点;阅读其他用户的个人资料，了解他们是否有匹配的兴趣，想法和想法;联系那些被认为是良好匹配的用户;从系统中注销我们假设每个帖子和回复都有一个链接，其中列出了所有相关的帖子和回复。用户可能有不同的动机来使用会议系统。一般而言，这些动机取决于用户动机决定了用户根据具体目标，用户可以利用系统提供的不同服务。在本文中，我们分析了与三个特定目标相关的用户行为：通过浏览发布的消息和用户个人资料收集信息;与代表良好匹配的用户建立联系;通过发布信息和回复信息（阅读后）来表达想法。2.2Web界面第2.1节中对用户与系统交互的非正式描述• 用户尚未登录;• 用户已登录，但尚未设置配置文件;• 用户设置了一个profile。我们假设A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）37(1) 只有登录的用户可以设置他们的个人资料和阅读用户个人资料和消息;(2) 只有设置了配置文件的用户才可以发布或回复消息并联系其他用户。因此，当用户登录、设置配置文件和注销时，用户状态会发生变化。系统界面由三个主要网页组成• 一个主页，用于设置用户配置文件和浏览有关会议的一般信息;• 浏览其他用户设置的用户个人资料的页面• 一个论坛页面，用于发布自己的消息和浏览其他用户发布的消息用户配置文件页面链接到• 配置文件页面，允许用户查看和分析特定配置文件，并在找到匹配项时联系相应的用户。论坛页面链接到• 允许用户阅读特定消息的消息页面，如果发现感兴趣，则可以回复该消息。这两个额外的页面是相互链接的，因为每个消息都有一个作者，他必须建立一个简介，由于上面的假设（2）。因此，消息与作者的个人资料相关联。类似地，如果相应的用户已经发布（或回复）任何消息，则简档可以链接到消息。3用户行为建模我们将在整个论文中使用的符号是基于Hoare我们对CSP使用• “• “• “X [|S|是进程X和Y与同步集S的并行组合。同步集合定义了在并行组合中必须同步的动作集合我们的用户行为模型集中在2.1节中介绍的三个用户目标上。用户心中的特定目标将驱动在Web界面允许的操作中选择适当的操作。例如，如果目标是收集信息，用户只需要浏览发布的消息和其他用户配置文件，而如果目标是建立联系人，用户最终需要明确联系另一个用户。为了实现任何目标，用户总是需要登录系统（第2.2节中的假设（1））。这8A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）3确保最初只有授权用户才能进入系统。proc User =（ login -> AuthorisedUser）[] UnauthorisedUserproc AuthorisedUser = goal ->（（ gather_info -> GatherInfo）[]（establish_contact->搜索联系人）[]（express_ideas ->搜索想法））完成目标后，授权用户可以注销或选择新的目标，并继续与系统的交互会话原则上，一个认知上合理的行为[1]必须包括这样一种情况，即用户可以在任何时候离开交互会话，而不管目标是否实现然而，当用户专注于实现目标时，这种情况不太可能发生，但在目标实现后，这种情况就更有 实际上，用户在目标实现时假设所有任务都已完成，但忘记完成一些重要的附属任务（完成后错误）[5]，例如注销系统。因此，我们假设，(1) 用户在试图实现目标时不会注销并且不会使交互会话无人值守，除非未能执行实现目标所需的动作;(2) 在实现目标之后，用户可能忘记注销并且使交互会话无人值守。proc GoalAchieved = AuthorisedUser[] Leaveproc Leave = unattended ->（（ short_delay -> UnauthorisedUser）[]（long_delay->UnauthorisedUser））[]（logout -> User）proc UnauthorisedUser =（ try_setup -> UnauthorisedUser）[]（try_contact->UnauthorisedUser）[]（try_reply ->UnauthorisedUser）[]（try_post_a_message->UnauthorisedUser）[]（try_read_a_message->UnauthorisedUser）[]（try_read_a_profile-> UnauthorisedUser）[]（success -> UnauthorisedUser）[]（failure->UnauthorisedUser）[]（logout -> User）在实现目标之后，授权用户可以追求新的目标（状态AuthorisedUser）或离开会话（状态Leave）。在后一种情况下，用户可以注销（操作注销）或使会话无人值守（操作无人值守）而不注销。一个无人值守的开放会话，经过一段时间后，可能很短（action short_delay）或很长（action long_delay），可能会被一个未授权的用户（处于UnauthorisedUser状态）接管，他可以尝试执行任何操作。请注意，（授权或未授权）用户可能只是尝试执行预期的操作;此类操作是否成功（操作成功）或失败（操作失败）取决于用户与之交互的系统3.1表达思想在论坛上发帖和回复已经发布的消息是表达自己想法的方式一般来说，可以通过发布消息（actiontry_post_a_message后跟success）或回复（action）来实现目标（actiongoal_achievedA. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）39try_reply 后 跟 success ） ， 可 能 是 在 读 取 这 样 的 消 息 之 后 （ actiontry_read_a_message后跟success）。 由于第2.2节中的假设（2），可能还需要执行try_setup操作。请注意，一般来说，即使我们假设用户在回复之前有阅读消息的意图，我们也可能发生的是，用户在回复任何消息之前阅读若干消息，然后，打算回复其中的一些消息，可能错误地回复先前未阅读的消息。proc_setup =（ try_setup -> success ->成功->成功[]failure ->（放弃想法[]离开））[]（try_post_a_message->（success-> goal_achieved-> GoalAchieved[]failure ->（删除想法[]Leave））[]（try_read_a_message ->（success ->删除想法[]failure ->（删除Ideas[]Leave）[]（try_reply ->（success -> goal_achieved -> GoalAchieved）[]failure ->（放弃想法[]离开））在交互的任何阶段，用户可能无法（动作失败）执行动作。有四种可能的方式，用户可以对这种故障作出反应(i) 尝试重复失败的动作（保持在状态“已完成的想法”并重复相同的动作）;(ii) 尝试另一种操作（保持在“想法”状态并执行不同的操作）;(iii) 使交互会话处于无人值守状态（移动到Leave状态并执行unattended）;(iv) 从系统中注销（移动到Leave状态并执行注销）。一般来说，反应的选择取决于用户3.2建立联系为了与匹配的用户建立联系，必须明确地联系该用户。一般而言，希望建立联系的用户可能已经在系统外部收集了所有必要的信息以选择匹配用户并使用该系统仅联系这样的匹配用户。proc_configuration-> proc_configuration-> proc_configuration-> proc_configuration[] failure ->（退出联系人[] Leave））[]（try_read_a_profile ->（成功->退出联系人[]failure ->（取消联系[]Leave）[]（try_read_a_message ->（success ->取消联系[]failure ->（成功-> goal_achieved ->GoalAchieved[]failure ->（关闭Contact []Leave）有两种方法可以收集信息来帮助选择匹配的用户：阅读其他用户的个人资料（action try_read_a_profile）和阅读消息（action try_read_a_message）。 希望建立联系的用户将继续阅读配置文件和消息（保持在状态“联系人”），直到匹配-在尝试联系这样的匹配用户（action try_contact）之前，找到匹配用户。然而，可以立即执行动作try_contact而不进行任何迭代10A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）3如果信息收集过程是在系统外执行的，则信息收集循环的。显然，goal_achieved动作必须在try_contact动作之前。由于第2.2节中的假设（2），可能还需要执行try_setup操作至于先前的目标，在交互的任何阶段，用户可能成功或失败地执行动作。3.3收集信息收集有关其他用户的信息可能不仅是选择匹配用户的手段，而且也是要实现的最终目标。 如果收集信息是用户的实际目标，则try_read_a_profile和try_read_a_message操作中的每一个可以是信息收集循环的迭代（处于GatherInfo状态）或者导致goal_achieved动作，当用户已经收集了所有需要的信息时执行该动作。proc GatherInfo=（try_read_a_profile->（success->（GatherInfo[]goal_achieved->GoalAchieved）[]failure ->（GatherInfo[]Leave））[]（try_read_a_message->（success->（GatherInfo[]goal_achieved->GoalAchieved）[]failure ->（GatherInfo[]Leave））4初始系统设计4.1用户权限第2.2节中突出显示的三种基本用户状态可以通过以下三种CSP过程进行形式化。proc Priviliges=（login ->（（noprofile -> enter ->NonMember））[]（profile-> enter-> Member）procNonMember =（try_setup-> success->Member）[]（logout -> Priviliges）[]（try_read_a_profile->NonMember）[]（try_read_a_message->NonMember）[]（success ->NonMember）procMember=（try_read_a_profile->Member）[]（try_read_a_message->Member）[]（try_post_a_message->Member ） [] （try_reply->Member）[]（try_contact ->Member）[]（logout ->Priviliges）[]（success ->Member）进程权限定义初始状态，即用户尚未登录的状态。用户登录后（操作登录），系统检查用户是否已经设置了配置文件（操作配置文件）或没有（操作noprofile）。 如果用户尚未设置配置文件，则状态更改为NonMember，否则更改为为会员。这两种状态定义了与2.2节中的假设（1）和（2）相对应的两种用户权限。操作enter的目的是移动到与适当的用户权限相对应的状态并激活web第4.2节中描述的接口。通过成功执行try_setup操作可以更改用户权限（ 从NonMember更改为Member）。操作注销返回到初始状态（特权）。A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）311请注意，建立个人资料是实现表达想法和建立联系目标所必需的，但不是实现收集信息的目标。4.2Web界面Web界面的模型由六种状态组成。proc接口1=（输入->Home 1）procHome1 =（ users ->UserProfiles1）[]（ forum -> Forum1）[]（try_setup -> success ->Home1）[]（logout ->Interface1）proc UserProfiles1 =（ forum -> Forum1）[]（try_read_a_profile -> success ->AProfile1）[]（home->Home1）proc AProfile1=（back_to_users-> UserProfiles1）[]（try_read_a_message -> success ->AMessage1）[]（try_contact -> success ->AProfile1）proc Forum1 =（ try_read_a_message -> success ->AMessage1）[]（ users -> UserProfiles1）[]（try_post_a_message -> success ->论坛1）[]（首页->首页1）proc AMessage1 =（ try_read_a_profile -> success -> AProfile1）[]（ back_to_forum -> Forum1）[]（try_reply -> success ->AMessage1）在初始状态（界面1）下，Web界面的主页由输入操作激活（以及随后更改为状态Home1），这将结束第4.1节中描述的检查用户权限的过程。其他状态对2.2节中描述的五个网页进行建模。 用户、论坛、主页、back_to_users和back_to_forum的操作允许用户自由浏览五个网页。请注意，操作注销只能从状态Home1进行。这意味着用户必须始终返回主页才能注销。由于注销和导航是通过点击按钮来决定的，我们隐含地假设用户永远不会失败执行这样的操作。因此，我们不需要将注销和纯导航操作表示为尝试（通过将它们的名称前缀为“try_“），也不需要将它们与成功或失败的操作相关联。4.3整体系统模型整 个 系 统 由 进 程 SEM1 表 示 ， 该 进 程 SEM1 由 用 户 权 限 （ 最 初 处 于 状 态Priviliges）、web界面（最初处于状态Interface1）和用户（进程User）的并行组合给出。proc =（（特权[|{输入，try_read_a_profile，try_read_a_message，try_post_a_message，try_reply，try_contact，try_setup，成功，注销}|]接口1）[|{登录，尝试_设置，尝试_阅读_一个_消息，尝试_阅读_一个_配置文件，尝试_联系人，尝试_发布_一个_消息，尝试_回复，注销，成功，失败}|]User）Priviliges和Interface1进程必须同步所有可以由Priviliges进程最终执行的操作，除了profile和noprofile，它们定义了由Priviliges进程建模的检查过程（它们是Priviliges的内部操作）。该过程起源于过程特权和12A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）3然后，接口1与用户进程组合。在第二个并行组合中，同步必须包括定义与界面交互的所有用户操作。请注意，我们还包括了失败动作，它不会发生在同步集合中的特权和接口1进程中（因此也不会发生在它们的并行组合中）。这可以防止整个系统执行故障操作，因此建模以下假设(1) 用户永远不会不执行在当前网页上立即可用的预期动作在第4.2节中，对注销和导航操作隐式地做出了这样的假设;在这里，它被显式地扩展到所有用户操作。该假设的目的是表明，第5.4节中所述的模型检查分析所捕获的设计弱点独立于用户在与界面进行单次交互时的能力。5改进系统设计在本节中，我们使用第4节中定义的对原始Web界面的分析突出了安全漏洞，这些漏洞在下一个版本中部分或全部被克服5.1安全威胁和保障措施根据第3节中的假设（3）和（4），用户将不会注销， 在实现目标之前，不会让界面无人看管，除非未能执行实现目标所需的操作然而，在实现目标后，用户可能忘记注销，并离开界面无人看管，而不回来使用它。这种情况可能导致违反安全。该界面的设计旨在最大限度地减少未授权用户利用无人值守会话访问配置文件（违反保密协议）或冒充登录用户（伪装）的可能性。理想情况下，我们希望无人值守的会话能够按时自动注销，以防止安全违规。然而，在实践中，我们可以引入保护措施，最大限度地减少安全违规的可能性，而不会在提供给用户的服务的质量和性能方面带来太大的下降。为了在安全性与服务质量和性能之间找到适当的平衡，分析用户与系统交互时的态度和行为至关重要。具体的态度和行为实际上可能会降低某些威胁的可能性，并增加其他威胁的可能性。例如，当计划的操作没有立即出现在当前网页上时，恐慌是一种态度，可能会另一方面，在实现目标后总是检查所有任务是否完成的态度会减少A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）313在离开会话之前忘记注销的可能性。因此，只引入保护措施以防止最可能的威胁是明智的，即在对用户态度和行为的特定假设下更有可能发生的威胁5.2安全属性我们的系统应该满足的一个重要要求是，打开的会话永远不会无人看管。满足这样的要求将绝对防止安全违规的发生。然而，陈述一个在很大程度上取决于用户 并且只能部分地受到界面约束用户行为的方式的影响。假设会话实际上可以以第3节中假设（3）和（4）所表示的方式无人值守违规 特别是，我们希望确保未经授权的用户不能访问其他用户C={try_read_a_profile，try_read_a_message}，或通过成功执行以下操作假装是已登录的用户（伪装）M={try_setup，try_post_a_message，try_reply，try_contact}.集合S=CM包含所有可能导致安全违规的行为根据假设（3）、（4）和（5），只有在达到目标后，才能让会话无人值守。由于我们的模型隐含地假设目标仅由授权用户确定，因此可能发生安全违规的关键时间间隔从goal_achieved操作开始，并在action处目标，当授权用户确定下一个目标时，或在操作注销时。事实上，在UnauthorisedUser状态下无法确定新目标，并且操作注销将退出UnauthorisedUser状态。使用prop secure=（A G（{goal_achieved} ->（{-success}W{goal，logout}）在CWB-NC语法中，原子公式有形式{action list}或{-action list};前者由任何出现在action list中的action满足，而后者由任何不出现在action list中的action满足。请注意，死锁进程满足~{action list}，其中~是否定连接符，但不满足{-action list}。 W时态运算符（弱直到）确保公式pWq为真当且仅当p永远连续为真或直到q为真。属性安全性防止在实现目标和追求新目标或注销之间发生操作成功，也就是说，它防止在14A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）3在实现目标和追求新目标或退出之间成功地执行。因此，财产安全保证，• 授权用户将始终能够注销或设置新目标;• 如 果 会 话 在 实 现 目 标 （ actiongoal_achieved ） 之 后 无 人 值 守（actionunattended），则可能接管会话的未授权用户不能成功地执行S中的动作。请注意，在公式secure中使用{-success}而不是~{success}可以确保在目标实现后发生的死锁会伪造安全公式。我们将在5.3节中通过检查界面是否支持某些受约束的用户行为来利用这一点。5.3约束用户行为我们系统的用户不应该是使用交互式系统的专家。事实上，他们中的一些人可能对计算机的熟悉程度很低。第3节中定义的用户行为模型是一个非常通用的模型，需要加以限制，以捕捉非专家用户的特定态度和行为。非专业用户在实现目标后的典型行为是寻找注销的方法，但如果在合理的时间后找不到方法，则最终使会话无人值守。这种行为可以通过如下定义的过程来强制执行。proc NonExpert =（ goal-> NonExpert）[]（home-> NonExpert）[]（users ->NonExpert）[]（forum -> NonExpert）[]（back_to_users->NonExpert）[]（back_to_forum->NonExpert ） [] （ 无 人 值 守 ->NonExpert）[]（logout -> NonExpert）[]（goal_achieved-> Finished）proc Finished =（ logout-> NonExpert）[]（无人值守->非专家）然后，该过程必须与系统并行组成，如下所示。proc EM1N =（EM1[|{goal，home，users，forum，back_to_users，back_to_forum，无人值守，注销，目标实现}|非专家）除了无人值守和注销之外，两个进程同步的任何其他动作都不能在goal_achieved动作之后发生，这与上述非专家用户的行为一致然而，即使在当前网页上有一个立即可用的注销机制（例如注销按钮），由注销过程定义的用户也当操作无人值守和注销都可用但选择无人值守时，会发生这种情况。 我们模拟非健忘用户的极端情况，他总是选择注销操作在goal_achieved之后可用时，即使打算之后追求另一个目标，也绝不会离开会话。这样的非健忘用户可以通过适当地将系统与如下定义的非健忘过程同步来定义。Proc NonForgetful =（goal_achieved -> logout -> NonForgetful）A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）315[]（goal -> NonForgetful）[]（logout ->NonForgetful）适当的同步是通过构成这个过程来实现的，这个过程作为一个约束，与如下所述的同步1N并行procEM1NR =（EM1N [|{goal_achieved，unattended，logout，goal}|[英语泛读材料由于两个组件还必须在无人值守时同步，而这不会发生在NonForgetful进程的行为中，因此无人值守的操作永远不会发生在复合进程中。请注意，在使用不允许在goal_achieved之后立即执行操作注销的系统组合NonForgetful约束时，这将导致死锁。5.4初步设计分析使用CWB-NC，我们可以验证安全性是否不适用于EM 1 NR系统。尽管引入了约束以确保用户总是记得在终止与系统的交互之前注销，但系统似乎不安全。NonForgetful和NonExpert允许的约束在goal_achieved之后，仅立即执行操作注销，但注销仅在进程Interface1的状态Home1中可用，该状态不能是执行goal_achieved之后Interface1立即处于 这导致在目标实现后立即出现僵局，从而伪造了安全。安全性不适用于非专家用户被约束为立即注销的IEEE1NR系统的事实表明，安全脆弱性不可能是由于用户的健忘，并且需要改进Web界面以解决非专家用户。问题是，注销不是在每个网页上可用，而只是在主页上。用户必须正确地从已实现目标的页面导航回主页。 这可能是相当具有挑战性的， 非专业用户。此外，每个网页上的注销按钮的存在将提醒用户注销，因此也解决了专家但健忘的用户。因此，我们通过在每个状态中引入注销操作来修改接口，如下所示。proc接口2=（输入->Home 2）procHome2 =（ users ->UserProfiles2）[]（ forum -> Forum2）[]（try_setup -> success ->Home2）[]（logout ->Interface2）proc UserProfiles2 =（ forum -> Forum2）[]（try_read_a_profile -> success ->AProfile2）[]（home->Home2）[]（logout -> Interface2）proc AProfile2=（back_to_users-> UserProfiles2）[]（try_read_a_message -> success ->AMessage2）[]（try_contact -> success ->AProfile2）[]（logout -> Interface2）proc Forum2 =（ try_read_a_message -> success ->AMessage2）[]（ users -> UserProfiles2）[]（try_post_a_message-> success-> Forum2）16A. Cerone，N.Elbegbayan/电子笔记在理论计算机科学183（2007）3[]（首页->首页2）[]（logout -> Interface2）proc AMessage2 =（ try_read_a_profile -> success -> AProfile2）[]（ back_to_forum -> Forum2）[]（try_reply-> success->AMessage2）[]（logout -> Interface2）定义复合系统的过程定义如下。proc =（（特权[|{输入，try_read_a_profile，try_read_a_message，try_post_a_message，try_reply，try_contact，try_setup，成功，注销}|]接口2）[|{登录，尝试_设置，尝试_阅读_一个_消息，尝试_阅读_一个_配置文件，尝试_联系人，尝试_发布_一个_消息，尝试_回复，注销，成功，失败}|]User）proc EM2N =（EM2[|{goal，home，users，forum，back_to_users，back_to_forum，无人值守，注销，目标实现}|非专家）procEM2NR =（EM2N [|{goal_achieved，unattended，logout，goal}|[英语泛读材料现在，我们可以使用CWB-NC验证系统5.5暂停一下IEEE2定义的接口的一个问题是缺乏对健忘用户的任何保护。虽然在每个网页上添加直接注销机制可以提醒用户注销，但用户仍然可能忘记注销。财产安全实际上并不适用于EQUEM2N。改善这种情况的一种方法是在接口中引入超时我们修改接口如下proc接口3=（输入->主页3）procHome3 =（ users ->UserProfiles3）[]（ forum -> Forum3）[]（try_setup -> success ->Home3）[]（logout ->Interface3）[]（short_delay ->Home 3）[]（long_delay -> timeout -> logout -> Interface3）proc UserProfiles3 =（ forum -> Forum3）[]（try_read_a_profile -> success ->AProfile3）[]（home->Home3）[]（logout -> Interface3）[]（short_delay-> UserProfiles3）[]（long_delay -> timeout -> logout -> Interface3）proc AProfile3=（back_to_users-> UserProfiles3）[]（try_read_a_message -> success ->AMessage3）[]（try_contact -> success ->AProfile3）[]（logout -> Interface3）[]（short_delay -> AProfile3）[]（long_delay -> timeout -> logout -> Interface3）proc Forum3 =（ try_read_a_message -> success ->AMessage3）[]（ users -> UserProfiles3）[]（try_post_a_message -> success ->论坛3）[]（首页->首页3）[]（logout -> Interface3）[]（short_delay ->Forum3）[]（long_delay -> timeout -> logout -> Interface3）proc AMessage3 =（ try_read_a_profile -> success -> AProfile3）[]（ back_to_forum ->
