非正式GUI设计：方法与技术结合实现用户界面管理系统的开发

理论计算机科学电子笔记183（2007）57-72www.elsevier.com/locate/entcs非正式GUI设计朱迪·鲍恩1，2 Steve Reeves3新西兰怀卡托汉密尔顿大学计算机科学系摘要软件系统的设计和实现有许多不同的方法。 这些方法可能是完全正式的，例如使用正式的规范语言和精化过程，或者它们可能是完全非正式的，例如在编码之前在纸上记下设计想法，或者它们可能在某个地方。在这两个极端之间。正式的方法自然适合底层系统行为，而以用户为中心的用户界面设计方法适合更非正式的方法。挑战在于找到将以用户为中心的设计方法与正式方法相结合的方法，以便充分实现两者的好处。本文提出了一种在正式环境中捕捉非正式设计工件背后的意图的方法，然后展示了这种方法的几个应用关键词：形式化方法，以用户为中心的设计，图形用户界面，细化，非正式设计工件。1介绍当我们设计和构建系统时，特别是大型和复杂的系统，以模块化方式工作并不罕见。系统的不同部分将在不同的时间进行工作，可能由不同的软件工程师、设计师和程序员团队进行。将系统的图形用户界面（GUI）的设计和实现与我们将称为底层系统行为的内容基于系统功能和用户界面（UI）的逻辑分离的用户界面管理系统（UIMS）的开发以Seeheim模型为例[20]。这种分离使我们不仅能够关注系统开发的不同部分所呈现的不同关注点，而且更重要的是，允许不同的方法和设计技术。1感谢DSV-IS 20062电子邮件地址：jab34@cs.waikato.ac.nz3电子邮件地址：stever@cs.waikato.ac.nz1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.06158J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）57当我们为一个应用程序开发底层系统功能时，我们经常关心的问题是正确性、可靠性、鲁棒性和效率等，这些问题都适用于我们称之为“形式”的技术此类正式技术包括规定要求、确认和验证规范和细化方法。然而，当我们开发UI时，我们的关注点往往更加以人为本（如果我们遵循以用户为中心的设计（UCD）方法，这一点尤其如此）。我们采用的设计技术反映了这一点，并依赖于更多的非正式策略，如原型设计，场景和故事板，基于用户反馈的迭代，可用性测试等。虽然我们可以看到这种关注点和设计方法的分离的好处，即能够对任务的不同部分采用最合适的开发方法，但显然存在一些与之相关的问题。如果我们的目标是使用正式的过程来开发可证明正确的软件（它是），那么我们必须确保系统的所有部分都以满足这一点的方式设计正式和非正式之间的这种差距已经被确认和讨论了很多次，特别是在1990年由Thimbleby [24]。近年来，不同的研究小组采取了几种不同的方法来试图弥合这一差距。已完成的大部分工作属于以下类别之一：• 为UI设计开发新的形式化方法。例如，使用新的形式主义建模UI [7];• 从现有的正式方法和/或非正式设计方法中开发混合方法。例如，结合交互器使用时序逻辑[17];• 使用现有的形式化方法来描述UI和UI行为。例如，UI设计的矩阵代数[25];• 用正式的基于模型的方法取代现有的以人为本的技术例如，使用Object-Z中的UI描述[23]来评估可用性[12]。虽然这些工作在将正式方法和UI设计结合在一起方面迈出了一步，但已经开发的方法和技术在大多数情况下都未能成为主流。这两个集团似乎都不愿意采用拟议的新方法，原因之一当然是任何集团都不愿意改变满足其各自需要的工作做法。说服正式方法的用户采用不那么正式的方法，或者新的混合方法，已经证明是不成功的，就像鼓励UI设计师放弃以人为本的方法，转而采用更正式的方法一样。与其试图改变不同软件开发人员群体所使用的方法，我们在研究中采取的方法是考虑现有的、不同的、正在使用的方法，并开发将它们正式联系在一起的方法。特别是，因为我们的兴趣在于使用正式的方法和严格的开发技术来开发我们的软件，以及UCD方法来进行UI设计，我们的目的是找到在我们的正式框架内解释UCD过程中产生的各种非正式设计工件的方法。J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）5759在本文中，我们将介绍一种正式描述非正式的设计工件的方式，称为表示模型。我们将给出一些在正式设计环境中使用表示模型的例子，然后展示如何用另一种形式主义，有限状态机来扩展这个模型。然后，我们可以开始探索构成模型基础的设计的静态和动态含义。2以用户为中心的设计作品以用户为中心的设计的目的是确保我们构建的软件，特别是与该软件的接口，满足预期用户的期望。为此，所使用的流程旨在让用户从早期阶段就参与进来，不仅要了解他们需要使用软件执行的任务，还要了解用户当前的工作实践，他们使用类似软件的经验，以及将受到新软件影响的公司内部工作流程等。在UCD过程中早期使用的技术可能包括人种学研究，使设计师不仅了解用户，而且了解他们的工作环境和工作流程。这之后可能是任务分析方法，以检查系统的用户多年来，任务分析受到了正式从业者的大量关注，并且存在许多模型，以及从这些模型开发UI的方法，例如[6]，[18]。UCD从业者可以使用场景和人物角色来增强任务分析过程，并提供专业需求和用户行为的详细信息。UI的实际设计可能涉及设计者和用户之间的头脑风暴会议然后，这些原型由用户和设计专家进行测试，并在最终设计之前进行迭代更新。一旦系统实施并随后进行可用性测试，即使是最终设计也会进行修改因此，UCD的关键是确保系统的实际用户参与设计过程的所有阶段。在这样的过程中产生的各种人工制品反映了这种协作的工作方式，包括白板设计会议和用于表示界面元素的便利贴，领域信息和场景的文本叙述性描述当我们试图在正式的软件工程环境中捕获UCD过程时，我们面临的问题之一是所产生的工件是故意非正式的。他们的目标是鼓励用户感觉能够参与和改变设计，而诸如纸上原型之类的大规模人工制品已经被在这方面非常成功。已经开发了几种方法和工具，支持原型设计或允许使用平板电脑[14]，协作白板[21]或台式计算机以类似于纸上原型设计的方式生成原型[8]。它60J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）57也许这些工具中的一些或全部可以调整或扩展，以支持我们目前正在做的工作。然而，由于我们目前的重点是现有的常用设计技术和人工制品，我们故意选择不在这里考虑这些工具。相反，我们专注于基于纸张的原型等高可靠性人工制品。3形式化方法与改进当我们说我们希望使用形式化方法作为我们系统推导的基础时，我们的意思是我们希望在任何抽象/具体的层次上构建模型，这对系统的开发人员来说是最自然和有用的，我们可以用“数学”精度来研究因此，通常情况下，我们希望用一种具有明确定义的属性的语言来构建我们的模型（编写我们的规范）：语法，语义和逻辑。如果没有前两个属性，我们就不能（没有定义良好的语法）将具体化与所有其他假象分开，或者（没有定义良好的语义）知道具体化意味着什么，即使我们在语法上知道我们有一个具体化。第三个要求，即我们要有逻辑，显然也是必要的：能够建立一个定义明确的规范是一个良好的开端，但我们还需要能够精确地研究这个规范，看看它的假设是什么，看看它有什么性质，看看它对系统产生了什么影响，等等，对于所有这些必要的事情，我们必须有逻辑。因此，我们的要求是广泛的，不是很繁重，让开发人员可以选择他们喜欢使用的语言（根据熟悉程度，适合任务等做出决定）。）只要它有我们的三个属性。3.1细化细化背后的想法非常简单，可以追溯到Wirth [26]。它基于能够在系统的不同模型之间移动而不会对用户在其功能或可用性方面对系统的看法或感觉产生任何负面影响的期望。举一个简单的例子，我们可以从一个使用集合的系统转移到一个使用数组的系统：这里我们从抽象转移到具体，从一个方便和有用的想法（集合）转移到一个面向实现的想法（可能包括太多的细节）。精化背后的这个原始思想已经被推广，这样我们就可以不仅考虑实现的不同，而且考虑模型抽象的不同层次，从具体化到实现。精化背后的基本直觉是[9]：替代性原则：用一个程序替代另一个程序是可以接受的，只要程序的用户不可能观察到替代已经发生。如果一个程序可以被另一个程序替代，那么第二个程序就被称为第一个程序的精化。J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）57614技术集成在形式方法中集成不同的语言和模型并不罕见（实际上，至少有一个完整的会议专门讨论这个活动，即IFM [13]）。核心思想是适当地使用不同方法的不同特征和优势。有时候，仅仅使用不同的形式主义来指定系统的不同部分或不同属性就足够了，但是当方法完全集成时，可以看到最好的效果，因此它们之间有形式上的联系，允许完全严格的开发。我们的目标是将正式和非正式过程正式地联系起来，以便我们获得严格规范和细化的所有好处，即能够证明系统的属性，并正式确保我们满足需求并最终实现正确的实现，同时受益于UCD过程的非正式设计方法，确保我们满足用户需求并开发可用的界面。在GUI设计中使用形式化方法并不是一个新的想法，并且已经采取了许多不同的方法。这些可能是沿着形式化设计过程的特定部分的路线，例如任务分析[19]，或者以形式化的方式描述GUI [10]，或者从形式化模型中导出实现[11]，[7]。然而，我们试图做的是研究现有的设计方法，即以用户为中心的设计，检查所使用的过程和人工制品的类型，并找到将这些纳入正式过程的方法。5表现模型表示模型用于正式捕获非正式设计工件的含义，例如场景、故事板或原型。这是一个刻意简化的模型，因为它所描述的非正式人工制品本身就很简单，也很容易理解。这一点很重要，因为它可以更容易地鼓励其他人采用和使用该模型。当我们谈论设计人工制品的意义时，我们谈论的是非正式人工制品描述的UI应该做什么，也就是说，如果它被转换成一个实现，它的行为将是什么。如果我们孤立地考虑一个基于纸张的原型，它的含义可能是模糊的;它需要一些支持信息或上下文来明确它的意图。当设计师向用户展示原型时，会讨论当与所示部件交互时原型将做什么。这就形成了我们所说的原型叙事，伴随的故事让用户了解它将如何工作以及各个部分的作用。这允许发生模拟交互，这使得用户和设计师能够评估所提出的设计的适用性。表示模型是一个正式的模型，它描述了一个非正式的设计人工制品方面的小部件的设计，并捕捉他们的意义。它是刻意抽象和高层次的。表示模型并不打算取代非正式的设计人工制品，而是作为一个桥梁之间的意义捕获的设计和正式的设计过程62J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）57用于系统功能。下面给出表示模型的语法5.1语法pmodel验证声明验证：：=PModel{验证码}+，WidgetName{ident}+，Category{ident}+，4Behaviour{ident}，用户定义：：={用户名是用户名表达式}+pexpr|产品名称：P2Pexpr|联系我们用户名：：=用户名小部件描述符：：=（小部件名称，分类或类型，（{行为描述}））小部件名称：：=标识符categorybehavior{Q}+表示一个或多个Q{R}R表示零或多个R一个合法的演示模型的例子是：P模型p q r小部件名称 aCtrlbCtrl cSel类别控制服务价值行为p是（aCtrl，CtrlControl，（eActionfActionn））（bCtrl，CtrlControl，（dAction））q是（cSel，SVal，（eAction fAction））r是p：q该模型描述了一个具有两个组件p和q的UI（其中这些组件可能是不同的窗口或UI的不同状态 整个UI（即 p和q的组合）由r描述，并且：运算符充当组合。p有两个widget，aCtrol和bCtrl，它们都是活动控件。与aCtrl关联的行为是eAction和fAction，对于小部件bCtrl，关联的行为是dAction。q有一个小部件cSel，它是一个具有eAction和fAction行为的SValtek。因此，表示模型r是p和q的所有小部件的组合，并描述了UI的所有可能行为4所使用的类别是基于[2]中的工作。J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）576315.2语义我们现在可以给出模型的语义。首先，我们可以将设计的完整模型描述为环境ENV。环境是从某个表示模型及其部分的名称（来自标识符的集合Ide）到它们各自的值的映射：ENV=Ide→值值=常数+P（常数×常数×P常数）常量={v |v是一个标识符。我们使用语义函数来建立环境的内容，并根据给定的语法来描述其结构[[]]：pmodel→ENVDc：声明→ENVDf：定义E2 →ENV→ENV Expr：E2pexprE2 →ENV→ENV[[Decl Def]]=Df[[Def]]（Dc[[Decl]]）Dc[[P] Model π1.. πn（1）WidgetName α1.. αn（2）Category 1.. （3）行为β1.. βn（4）]]={πi <$→πi}n（1）<${αi<$→αi}n（2）<${βi <$→βi}n（3）<${βi<$→βi}n（4）1 1 1 1其中{ei}k是集合{e1，e2，. 、.、ek}Df[[D Ds]]ρ=Df[[Ds]]（Df[[D]]ρ）Df[[P is]]ρ=ρ{P<$→Expr[[]]ρ}其中ρ表示当前环境。Expr[[E Es]]ρ=Expr[[E]]ρExpr[[Es]]ρExpr[[：φ]]ρ=Expr[[]]ρExpr[[φ]]ρ表达式[[（N C（b1.. bn））]]ρ={（ρ（N）ρ（C）{ρ（b1）.. ρ（bn）}）}Expr[[I]]ρ=ρ（I）我们的表示模型由具有名称、类别和行为的小部件组成在我们的语义中，我们已经展示了模型的语法如何创建从标识符到环境中常量的映射（这代表了模型派生的设计）。表示模型语义是集合论的保守扩展，也就是说，从语义中可以证明的关于表示模型的一切都已经可以在集合论中使用语义方程中给出的定义来证明。这就允许我们依赖集合论现有的合理逻辑，为我们的表示模型导出一个必然合理的逻辑。接下来，我们将提供一个UI设计和该设计的表示模型的示例，我们将使用该示例来说明表示模型的使用和扩展64J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）576例如Fig. 1. 手机应用程序界面下面的例子是Calvery等人在[5]和[4]中给出的例子的改编。该示例涉及一个家庭加热控制系统，该系统可通过几种不同的设备访问，即基于家庭的壁挂式控制面板、在标准PC上运行的该控制系统支持对多个不同房间的温度进行监测和控制，为了我们的示例的目的，我们使用移动电话应用程序UI的修改版本，它允许我们说明我们的特定点。图1中给出了系统的移动电话版本的建议UI设计。这显示了组成应用程序UI的四个不同屏幕，我们分别标记为C1， C2， C3和C4移动电话UI设计的表示模型如下（为简洁起见，省略了一些细节）：PModel MPHeat MPMenu MPBed MPLamp MPBathWidget nameSelect LoungeSelect BedSelect QuitOpt Incampus OptDecember Opt IncLoungeOpt DecLoungeOptIncBedOptDecBedOpt Accept Opt CancelOptDecember TempDispRangeDisp LoungeTempDispLoungeRangeDisp BedTempDisp BedRangeDisp类别ActCtrl SValSel SValRespdr行为ShowBath ShowLounge ShowBed QuitApp IncampusTemp DecampusTemp IncLoungeTemp DecloungeTempIncBedTempDecBedTemp StoreSettings ShowMenuPageDispampusTemp Dispampus Range DispBedTemp DispLoungeTempDispLoungeRangeMPMenu为（选择，ActCtrl，（ShowBath））（LoungeSelect、ActCtrl、（ShowLounge））J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）5765房间当前温度：温度当前温度≤最大温度当前温度≥最小温度（BedSelect，ActCtrl，（ShowBed））（QuitOpt，ActCtrl，（QuitApp））MPBed是（BedTempDisp，SValRespndr，（DispBedTemp））（BedRangeDisp，SValRespndr，（DispBedRange））（IncBedOpt，SValSel，（IncBedTemp））（DecBedOpt，SValSel，（DecBedTemp））（AcceptOpt，ActCtrl，（StoreSettings））（CancelOpt，ActCtrl，（ShowMenuPage））MPL是... 省略MPBath是... 省略MPHeat是MPMenu：MPBath：MPLBed：MPBed7使用演示模型7.1表示模型和细化我们对演示模型的第一个用途是使我们能够将UI的设计纳入我们的正式细化流程。我们之前已经详细介绍了这个过程[3]，我们不打算在这里重复这些细节。然而，我们将给出一个过程的大纲，并将感兴趣的读者引导到[3]。我们已经讨论了正式和非正式设计过程活动之间的关系。我们在每个方法的第一个设计活动中开始定义它，即为正式规范收集需求并确定UI设计的用户需求。我们需要确保从每一个活动中收集的信息一起使用，以产生规范和UI需求，而不是单独对待这两个活动，这些规范和UI需求不仅是完全包容的，而且共享一个词汇表并相互补充。我们为系统创建一个正式的规范，并使用命名约定来指示哪些给定的操作是用户操作，也就是说，哪些对系统状态的操作应该通过UI直接提供给用户。如果我们要为加热应用创建一个正式的规范，基于[5]中给出的要求并使用规范语言Z [1]，我们将遵循此约定并相应地命名我们所描述的操作例如，为了描述用户能够增加的要求，任何房间的温度，我们希望在我们的规范中看到以下内容（使用Z推广习语）：TempControlSystem=^[roms：Rid→会议室]66J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）57增加室温Δ房间newTemp？：温度newTemp≥MinTempnewTemp≤MaxTempCurrentTempJ=newTempIncBedTempOpΔ卧室iActValue？：TEMP iAction？：行动iAction？=IncBedTempbedTempJ=iActValue？iAction？/=IncBedTemp床温J=床温Φ更新室温ΔTempControlSystemΔRoom摆脱？：RID摆脱？∈domroomsΘRoom =roomsrid？房间J=房间n {rid？›→会议室J}USERIncRoomTemp=^NΔR oom·ΦUpdateRoomTemp增加室温作为我们改进过程的一部分，我们需要确保规范中描述的所有用户操作已在UI设计中描述。也就是说，我们应该确保GUI设计非正式描述的系统是规范的细化。从设计的表示模型中，我们可以生成一个Z描述（使用[2]中给出的Z中描述小部件类别的框架作为基础）。从手机加热应用的呈现模型中，如果我们专注于提高卧室温度的要求，我们可以看看导出的Z描述的一部分，即：J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）5767^IncBedTempSelCtrliCState：控制状态iSelValue：TEMPiAction！：ACTIONiActValue！：温度iCState=活动状态iAction！=IncBedTempiCState=非ActiveIncBedTemp= [IncBedTempSelCtrl|iCState = Active]公司简介本例的表示模型描述了一个类别为SValResponder的小部件BedTempDisplay。如果我们参考[2]，我们看到要在Z中描述这样的小部件，我们必须提供一个模式，其中包含对活动状态的观察（捕获用户交互的概念），选择的值和行为，然后将其链接（使用Z管道符号）到描述相关行为的操作模式（在这种情况下将温度设置为新值）。我们现在可以使用标准的模拟技术（基于[27]和[9]）来证明UI设计和规范之间的关系。7.2表示模型和设计等效性在使用表示模型的基础上，我们再次基于表示模型推导出了设计之间的等价性这里的目的是能够采用不同的UI设计（对于同一个系统），并使用这些设计的表示模型来确定它们是否可以在某种程度上被认为是等效的。设计等效性在细化过程中很重要，设计的快速迭代意味着只有当设计发生重大变化时，即当它在功能上不再等同于先前版本的设计时，才要求证明细化到规范可能更实用。接下来，我们来定义这个功能等价的概念设计的功能由该设计的表示模型的行为集给出因此，如果我们希望比较两个不同的UI设计，以确定它们是否具有相同的功能，那么我们可以简单地比较它们的表示模型的相应行为集。我们正式声明：定义7.1如果DOne和DTwo是UI设计，PMOne和PMTwo是68J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）57其相应的表示模型则：DOne函数DTwo=df行为[PMOne]=行为[PMTwo]行为[P]= df{[[P]] b |b ∈ act（P）}act（P）是一个语法函数，返回P中行为的所有标识符。在我们为不同版本的系统设计多个接口的情况下，设计等效性也很重要，就像我们在家庭供暖系统的例子中一样。我们希望确保系统的不同版本为用户提供相同的功能。同样，我们可以通过使用从每个不同系统设计到规范的细化技术来证明这一点。然而，设计等价提供了一种较弱的细化方法，使我们能够确保所有UI都提供了预期的行为（系统功能行为和UI功能行为）除了功能等价，我们还考虑了设计之间存在的其他类型的等价，即组件等价和同构。我们不会在这里详细讨论这些类型的等价，因为它们超出了本文的范围。7.3表示模型和设计一致性我们在这里介绍的表示模型的第三个用途是确保设计之间的一致性。一致性是UI设计的一个重要原则。Shnei- derman [22]将一致性作为界面设计的八条黄金法则之一努力保持一致性。在类似的情况下，应该要求一致的操作序列;在提示、菜单和帮助屏幕中应该使用相同的术语;并且应该始终使用一致的命令。一个应用程序可能由许多不同的屏幕和对话框组成，因此始终保持一致性并不是一项微不足道的任务。使用表示模型，我们可以确保的一件事是，具有相同功能的控件具有相同的名称（因此用户不必记住，在界面的一部分，他们使用Quit退出界面，而在另一部分，他们使用Close）。相反，我们也可以再次使用模型来检查具有相同名称的控件是否具有相同的功能，这确保了用户总是知道当他们遇到这样的控件时会发生什么。8限制和扩展我们已经提供了一些例子，说明如何使用非正式设计的表示模型，不仅有助于实现将非正式设计工件集成到正式过程中的目标（通过细化机制和等价性），而且还有助于处理设计问题，如一致性。J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）5769然而，关于细化的问题，还有更多的话要说。虽然我们可以证明（或反驳）特定的功能包含在UI设计中正如我们已经说过的，一个UI可能由许多不同的窗口和对话框组成。在这些不同窗口或对话框之间移动的机制包含在设计的UI功能中（这些行为与底层系统功能不对应，而是用于更改UI的状态）。对于规范和设计之间的细化，我们需要确保不仅所需的系统功能存在于UI设计的某些部分，而且它们可以通过某些UI功能访问在UI中证明可达性的属性是在UI中使用形式化方法的早期工作中的一个共同关注点。我们希望能够使用我们的表示模型来实现这一目的，而不是试图将现有的技术适应并合并到我们的过程中。试图通过表示模型来捕捉UI的动态变化的想法的问题在于，该模型为我们提供了设计的静态视图。 它描述了由设计给出的总环境（我们可以认为是该设计的所有可能性），但是（故意）简单地使用每个小部件的三元组并没有保持足够的信息来扩展其使用到动态的。一个可能的解决方案是用额外的信息扩展模型然而，我们希望避免使它变得如此复杂，以至于它成为设计师或正式从业者学习和使用的负担。我们决定使用另一种常见的形式主义，结合表示模型，以便能够证明这些更动态的属性。我们选择的形式主义是有限状态机（FSM）。FSM以前曾被用于GUI设计建模（早在20世纪60年代末以这种方式使用FSM的缺点之一是已知的状态爆炸问题，其中机器的状态数量变得难以控制地大。考虑到现代UI的复杂性，无论何时我们尝试使用FSM来建模GUI或GUI行为，这肯定是一个关注和潜在的问题。然而，因为我们已经有了UI（表示模型）的抽象，所以我们可以将其与FSM结合使用，并且在大多数情况下，我们生成的FSM只需要非常少的状态。我们产生一个FSM，它是在一个高的抽象层次，用提供较低层次含义的表示模型来装饰它我们的FSM概念包括：状态的有限集合，Q;输入数据的有限集合，N;转换函数δ，它接受一个状态和一个输入标签，并返回一个状态（q→a→qJ）;一个起始状态q0，Q中的一个状态。 FSM则为4tup le（Q，θ，δ，q0）.Q中的每个状态都与FSM描述的整个模型中的表示模型的名称相关联。当FSM处于特定状态时，则与该状态相关联的表示模型是当前活动的表示模型，即该 模 型 中 描 述 的 UI部分对用户可见且可用70J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）57图二. PIM for MPHeat演示模型for interaction互动.我们可以清楚地将FSM的定义扩展到五元组，并添加从状态名称到表示模型名称的映射，以正式显示这一点协会中的输入标签本身就是所采取的行为的名称从表现模型的行为集合中。通过这种方式，我们可以将设计部分的UI功能与动态行为相关联，从而使用户可以使用界面的不同部分。我们把这种表示模型和有限状态机的结合称为表示和交互模型（PIM）。我们对FSM的良构性定义如下：表示模型的PIM是格式良好的，其中任何状态的转换上的标签是存在于与该状态相关联的表示模型的行为集中的行为的名称。使用FSM的符号，我们可以更正式地给出它：<$（q，t，qJ）：δ·<$b∈act（qPModel）·t=b其中qPModel是与状态q相关联的表示模型。如果我们再次回到图1中给出的基于手机的应用程序的设计，我们可以看到，在我们考虑这个UI的功能的可达性之前，我们需要捕获我们从界面的一个部分移动到另一个部分的方式通常，原型被注释以包括这类信息（或者在故事板的情况下，这隐含在图的流程中）。我们使用FSM来捕获UI各部分之间隐含的动态行为，我们用表示模型的各部分来装饰FSM图2给出了图1设计的PIM。现在，为了证明一个特定的行为是可达的，我们首先需要证明它所在的UI部分（即在其行为集中包含该行为的组件表示模型）本身在FSM中是可达的，这可以使用标准FSM方法来证明。J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）57719结论在本文中，我们已经描述了如何帮助整合正式的方法与非正式的UI设计方法。这种方法涉及到创建一个正式的非正式的设计工件的方式，使我们能够在正式的过程中使用它们。我们已经描述了表示模型，它正式捕获了非正式的UI设计，并讨论了如何使用它将设计纳入正式的细化过程以及设计等价性和一致性检查。表示模型允许我们捕获UI设计的静态属性，我们随后展示了如何使用它与另一种形式主义，FSM，以捕获基于UI功能的动态UI行为，这些UI功能改变了用户的UI可用功能，给出PIM。我们提出的表示模型和方法的主要优点是，它们可以与正式从业者和设计人员使用的现有方法结合使用。我们并不要求这些团体放弃他们现有的方法和技术，而是用一种相对简单的形式主义和一套与他们现有的方法一起工作的技术来增强这些方法和技术，而不是取代他们现有的方法。本文旨在概述我们的工作和技术，而不是详细介绍其中的一个特定部分我们已经描述了我们在这一领域的一般工作，并在适当的地方，我们建议读者在以前的出版物中更在形式化方法和UI设计领域已经做了大量的工作，这比我们在本文中所能考虑的要多。我们已经尝试引用适当的著作，并在相关的地方解释我们方法中的差异，但这些参考文献绝不应被视为详尽的清单。引用[1] ISO/IEC 13568。信息技术-Z形式规范表示法-符号、类型系统和语义。普伦蒂斯-霍尔国际计算机科学系列。ISO/IEC，第一版，2002年。[2] 朱迪·鲍文。用户界面设计指南的正式规范。硕士论文，计算机科学系，怀卡托大学，2005年。[3] 朱迪·鲍文和史蒂夫·里维斯。非正式GUI设计工件的正式细化。澳大利亚软件工程会议（ASWECIEEE，2006年。[4] G. Calvary， J. Coutaz ，and D.戴维 宁支 持塑料 用户 界面的 上下文 更改 ：一 个过程 和一 种机制 。以 .Blandford，J. Vanderdonckt和P. Gray，编辑，HCI'2001和IHM'2001的联合会议记录Springer-Verlag，2001.[5] GaelleCal vary，Joel le Coutaz，andDavidTheve nin. 为开发塑料用户界面提供了一种全新的保护。在EHCI史普林格出版社[6] 我是一个很好的朋友，我是一个很好的朋友，我是一个很好的朋友。支持多个开发接口的可扩展开发操作。EHCI/DS-VIS，第346-362页[7] 安东尼·考特尼。功能建模的用户界面。在互动系统。设计、规范和验证。2003年第10届DSV-IS国际研讨会，丰沙尔，马德拉岛（葡萄牙）J.Joaquim，N.Jardim Nunes，J.Falcao e Cunha（ed.）第107Springer Verlag Lecture Notes inComputer Science LNCS，2003。72J. Bowen，S.Reeves/Electronic Notes in Theoretical Computer Science 183（2007）57[8] Adriencoyetete ， St'ephane我 的 名 字 是 Faulkner ， ManuelKolp ， QuentinLi mbourg ，andJeanVanderdonckt. 基于usixml的用户界面草图多代理设计工具。在TAMODIAPress.[9] 约翰·德里克和艾克·博滕。Z和Object-Z中的细化：基础和高级应用。计算与信息技术的形式化方法Springer，May 2001.[10] David J. Duke、Bob Fields和Michael D.哈里森用户界面设计方案的规范和分析案例研究。正式ASP.Comput. ，11（2）：107[11]D. F. Gieskens和J.D.福利 通过前置条件和后置条件控制用户界面对象。在Proc. 的CHI-92，第189-194页，Monterey，CA，1992。[12] A.于西岛MacColl，和D.卡林顿从正式的用户界面设计评估可用性。技术报告TR 00 -15，软件验证研究中心，昆士兰大学，2000年。[13] IFM05. http://www.win.tue.nl/ifm/，2005年。[14] J. 兰迪Silk：像Krazy一样绘制界面在计算系统中的[15] A. Paiva，N.Tillmann，J.Faria和R.维达尔建模和测试分层GUI。 In D. 博基耶，E. Borger和A. Slissenko，editors，ASM05，pages 329-344.巴黎大学，2005年。[16] David L.帕纳斯交互式计算机系统用户界面设计中转换图的使用。1969年第24届全国会议论文集，第379-385页。北京：人民出版社，1969年。[17] F. M. 我不吃，先生。S. Sciaccitano和J. Lowgren. 一个有用的函数将物理上的用户操作应用于任务驱动的形式化规范。交互系统的设计、规范和验证，第155-173页。Springer Verlag，1995年。[18] 我不吃。在这两个系统的内部控制中，需要进行大量的修改。软件工程与知识工程手册，2001。[19] 我不 吃。下 面是一个针对特定系统的UML。InEHCI'01：Proceedingsofthehe8thIFIPInternationalConferenceonEngineeringforHuman-ComputerInteraction，pages 7-18，London，UK，2001. 史普林格出版社[20] G. E. Pfa 用户界面管理系统。 Springer-Verlag New York，Inc. 一九八五年[21] 贝丽尔·普利默和马克·阿珀利计算机辅助草图捕捉初步设计。 在CRPIT澳大利亚计算机协会[22] 本·施奈德曼设计用户界面：有效的人机交互策略。Addison Wesley Longman Inc，第3版，1998年。[23] 格雷姆·史密斯。 Object-Z Specification Language。 Kluwer Academic Publishers，2000.[24] H. Thimbleby. 交互系统的设计软件工程师[25] 哈罗德·辛布尔比用矩阵代数设计用户界面。ACM传输计算- Hum.互动. ，11（2）：181[26] 尼克劳斯·沃思逐步细化的程序开发。Communications of the ACM，14（4）：221[27] 伍德考克和戴维斯。 使用Z：规范，改进和证明。Prentice Hall，1996年。