基于模型的Web应用程序可用性评估方法的研究

理论计算机科学电子笔记157（2006）207-211www.elsevier.com/locate/entcs什么样的形式化导航模型的可靠性和可用性的Web应用程序的验证？Marco Winckler1 Eric Barboni2 Philippe Palanque3Christelle Farenc4LIIHS-IRITUniversity PaulSabatierToulouse，法国摘要在本文中，我们简要介绍了一种专门用于Web应用程序模型导航的符号我们讨论了一些策略来评估导航模型的可用性，一个符号我们进行这种评估的目的是确保（在实现之前）重要的用户任务可以（或不能）使用系统执行关键词：基于模型的Web开发，基于模型的验证，形式化描述技术，可用性评估。1使用SWC符号的基于模型的设计是Web上相对较新的领域，但由于构建越来越复杂的Web应用程序对建模支持的需求，它正在快速增长[6]。然而，即使存在适当的建模技术，单独使用建模方法也不足以确保Web应用程序的可用性和可靠性可用性评估不是1电子邮件地址：winckler@irit.fr2电子邮件地址：barboni@irit.fr3电子邮件地址：palanque@irit.fr4 电子邮件地址：farenc@irit.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.056208M. Winckler等人/理论计算机科学电子笔记157（2006）207不仅对于在开发过程的早期阶段识别问题很重要，而且对于管理在web应用上执行的频繁更新也很重要。为 了 克 服 非 正 式 模 型 的 局 限 性 ， 我 们 提 出 了 StateWebCharts（SWC）[9]符号来描述Web应用程序的导航。SWC是一种正式的符号，通过为状态和转换添加适当的语义来扩展StateCharts [5]，包括对话主动控制和客户端和瞬态活动等概念更一般地，网页（静态或动态生成的）与SWC状态相关联因此，每个状态描述了用户在应用程序上导航时可以看到哪些对象。链接由状态之间的转换表示。数据可以通过转换从一种状态转移到另一种状态持久性数据可以由一种特殊的状态来保存，称为瞬态。SWC状态的操作语义是：当前状态及其容器对用户可见，而非当前状态是隐藏的。用户只能从当前状态导航传出关系（由模型中的转换方式表示）。当用户选择一个转换时，系统会离开源状态，使其变为非活动状态，让目标状态成为配置中的下一个活动状态。图1提供了SWC表示法的概览，该表示法呈现了对小型搜索引擎进行建模的导航。在状态“S1”上以黑点开始的装饰指示初始状态。这种初始状态的概念以及许多其他构造都是StateCharts的继承。外部状态（例如外部状态是必要的，因为指向其他Web应用程序的链接应被视为设计的一部分。类似地，SWC提供其他类型的状态来表示可能包括动态内容，该动态内容包含在设计时不能确定的导航路径（例如，“S3”）。状态“S2”表示通常表示系统发动机的瞬态。虚线箭头（例如，“t3”、“t2”）指示由系统触发的转变，而连续箭头（例如，“t1”、“t4”、“t5”）标识由用户事件触发的转变。SWC符号的详细描述可以在[9]中找到M. Winckler等人/理论计算机科学电子笔记157（2006）207209Fig. 1. 导航建模与SWC的一个小型搜索引擎。2基于模型的导航评估策略在过去的一年中，已经提出了几种方法来支持基于模型的评估，如模型检查[1]和系统属性检查[2]。在本节中，我们简要介绍了4种评估导航模型可用性的策略：a）静态验证; b）动态验证; c）系统属性验证; d）使用用户场景评估导航模型。我们的目标是讨论每种方法的潜在好处，相对于Web应用程序的开发静态验证是指不执行模型的分析。如[2]中所述，已经提出了几种方法来支持基于模型的评估，例如模型检查（通常用于软件测试，用于检查模型的内在元素）[7]。这一类别涵盖了以下问题：a）模型一致性; b）不可达状态; c）悬挂链接; d）链接冗余; e）不可达路径; f）最短路径;g）强制路径; h）数据依赖性。动态验证的原则是，必须执行或模拟模型才能执行验证。在设计者的控制下，模拟一步一步地进行，可以用作一种检查导航规范及其相应Web应用程序的漫游方法。在这种情况下，设计师像真实用户一样“导航”模型。这个任务可以通过适当的工具支持来减轻。遍历模型并不是执行动态验证的唯一方式，因为导航模型也可以被访问以测量给定的测试套件或测试用例的集合。 测试服由一套自动化工具用来检查模型的指令[1];例如：a）在某个测试用例中，每个状态至少被访问一次; b）每个状态的每个关系至少被跟踪一次;站点中的每个路径至少在一个测试用例中被跟踪。210M. Winckler等人/理论计算机科学电子笔记157（2006）207属性的验证是通过检查模型来完成的，以验证模型是否与某些预定义的行为规则（因为我们在本文中只考虑导航所涉及的属性）兼容。它们可以通过使用时态逻辑[3]或任何其他抽象声明形式描述技术来表达。属性可以是非常通用/抽象的，也可以是非常具体的，例如这种属性可以在模型上自动验证，甚至嵌入到编辑器工具中，但这在很大程度上取决于符号的表达能力和模型的复杂性。到目前为止，只有很少的工作[4]已经致力于验证人机工程学规则作为模型的属性。使用用户场景评估导航模型的目的是利用两个互补的模型，并交叉检查它们的兼容性。任务模型的目的不仅是描述用户如何执行任务，而且还描述何时以及为什么执行这些任务（为了实现哪个目标）。任务模型通常是详细说明接口功能需求的结果，描述了应用程序的用户任务。这种评估的基础是从任务模型中提取场景，并在导航模型上播放它们[10]。与其他分析导航路径的工作不同，这个过程允许设计师将导航路径与实际任务进行比较，这应该能对Web应用程序用户界面的可用性提供更深入的了解3讨论和今后的工作正如Campos和Harrison [2]和Farenc [4]所讨论的，可以将基于模型的评估结果与交互系统的可用性原则相关联。模型的静态属性的验证在形式方法的学科中有着悠久的传统，并且为此目的存在许多工具。通过模拟对模型进行动态验证也被用于评估Web应用程序的导航[7][8]。目前，基于模型的导航模型评估的主要缺点涉及动态内容生成和用户导航目标的识别。内容的自动生成可能包括新的链接，这些链接可以修改在导航模型上执行的评估所预测的可用性。目标驱动的评估不能仅仅使用导航模型来解决，因为我们不能将导航路径与单个用户目标相匹配。事实上，用户通常可以遵循许多导航路径来实现相同的目标。如果我们将从任务模型和导航模型中提取的场景M. Winckler等人/理论计算机科学电子笔记157（2006）207211正如我们在[10]中所证明的那样。我们在这项正在进行的研究中解决的主要问题之一是确定建模方法的哪些要素可用于评估目的。从这个意义上说，我们已经为SWC元素提出了一个特定的语义，例如，允许通过所谓的动态状态和导致系统状态变化的代理的正式表示来识别内容生成，这对于评估对话的控制至关重要。SWC表示法还提供了处理上述评估所需的关于状态、关系和事件的所有基本信息集。SWCEditor支持SWC模型的编辑[8]这也允许模型的模拟和验证。我们正在进行的工作包括开发分析工具并将其集成到我们的原型中，以支持繁琐且需要资源的手动过程。引用[1] Beizer，B.，软件测试技术（第二版）Van Nostrand Reinhold Co. 1990年[2] 坎 波 斯 ， J.C. 和 M. Harrison ， Formally verifying interactive systems ： a review ， in ：Design，Specification and Verification of Interactive Systems109-124[3] Emerson，E. A. J. Srinivasan，分支时间时序逻辑，在：线性时间，分支时间和偏序逻辑和模型的并发性，学校/研讨会（1989年），页。123-172.[4] 法伦茨角，澳-地P. Palanque和R.在交互式软件开发过程中嵌入人机工程学规则作为一般要求。Interact 99第七届人机交互国际会议，1999年，第100页。408-416[5]哈雷尔，D.， Statecharts：计算机系统的可视化形式。Sci. Comput. 程序. 8（1987），pp. 231-274。[6] Murugesan，S.和Y.Deshpande，editors，[7] Ricca，F.和P.Tonella，Web应用程序的分析和测试，在：ICSE25比34[8] Winckler，M.，E.巴尔博尼角Farenc和P. Palanque，Swceditor：一个基于模型的工具，用于网络导航的交互式建模，在：计算机辅助用户界面设计国际会议- CADUI55比66[9] Winckler，M. P. Palanque，Statewebcharts：A formal description technique dedicated tonavigation modeling of web applications. ，in：DSV-IS，2003，pp.61比76[10] Winckler，M.，P. Palanque，C. Farenc和M. S. Pimenta，基于任务的网页导航设计评估，TAMODIA161比169