没有合适的资源?快使用搜索试试~ 我知道了~
97理论计算机科学电子笔记43(2001)网址:http://www.elsevier.nl/locate/entcs/volume43.html16页走向整合的认知与界面分析霍华德·鲍曼1计算实验室肯特大学坎特伯雷分校坎特伯雷,肯特,CT2 7NF,英国Giorgio Faconti和Mieke Massink2,3CNR-Istituto CNUCEVia V. Alfieri 1,Loc. Ghezzano -56100比萨,意大利摘要使用认知架构来分析人机界面的可用性是一个广泛研究的策略。执行这种分析的一种特别强大的方法是通过联合建模,其中接口和所选择的认知模型都在同一个规范框架中描述;允许分析两者的组合行为。本文提出LOTOS作为一种联合建模语言。我们强调了联合建模如此困难的四个原因,并展示了LOTOS符号如何解决这四个原因。1介绍形式化方法的构想是考虑到在计算系统开发过程中的应用。然而,由此产生的技术可以更普遍地被视为方法,写抽象(非规定性)的描述系统的行为,然后正式分析这些描述,以确定其涌现的属性,在这里系统一词是在一个非常普遍的意义上使用。在某种程度上,正式方法的这种更普遍的适用性已经得到了承认,这些技术的“非标准”应用已经取得。例如,有应用到建模(关键)1 电子邮件:H. ukc.ac.uk2电子邮件:G. cnuce.cnr.it3 电子邮件:M. cnuce.cnr.it2001年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-N D链接。98程序和文件,分析生物系统和计算机接口[13]。这里介绍的工作适合这些非标准应用中的后者。然而,我们的应用程序的形式化方法,人机交互是不寻常的,因为它侧重于syndetic建模-一种特殊的方法来分析计算机接口的可用性,其中的界面和用户的认知在本文中,我们认为,形式化描述技术LOTOS可以有利地应用到这样的联合建模。人机交互。 下一代人机界面将是极其复杂的,包括复杂的交互机制,如手势和多模式交互。此外,很明显,如果以不受约束的方式使用这些交互机制,则作为示例[10,9]显示了MATIS系统[18]中基于鼠标的指向手势和口语短语的组合如何由于竞争认知资源的需求而不像预期的那样有效。因此,有一个明确的需要,以评估如何认知要求特定的互动任务。这种评估的标准方法是构造一个原型系统实现并进行用户试验。然而,这既耗时又昂贵。因此,与许多其他人一起,我们考虑如何使用认知模型进行这样的评估。这种评估的一种有效方法是描述接口和所选择的认知模型,然后分析特定界面背景下的认知行为。术语联合建模已被用来描述这种组合的规格和分析[10,9,8]。然而,这种规范和分析的综合方法要求非常高。我们尤其可以强调以下四个主要困难:(i) 一般规范原则必须确定一种描述符号,该符号适用于对认知行为和界面行为进行建模这种探索的关键是找到(ii) 对认知行为首先,认知行为在本质上是高度复杂的,其次,我们对它的理解,如现有的认知架构所代表的,还远远没有完成。因此,给出认知行为的完整描述肯定是不可能的,必须采用适当的抽象。(iii) 扩展性虽然这是一个明显的需求,但对可伸缩性的需求是没有的。99怀疑批判特别是,任何非平凡的认知体系结构的完整描述将必然非常庞大,此外,界面行为可能极其复杂。因此,联合规范肯定会有两个主要(大)成分,每个成分都包含子成分。在解决这个可扩展性问题时,我们寻求具有两个特征的特定结构化技术:(a) 作曲。 我们希望能够通过添加新的组件来以组合的方式构建规范,而不必打破现有组件的封装。(b) 等级制度。支持可伸缩性的一个主要方面是以分层方式构建规范的能力,例如,在特定的分解级别,能够将复杂的行为包装在组件中,并在更高的规范级别上使用生成的组件。这意味着我们需要允许组件本身按照组件进行结构化。请注意,有些技术在这方面失败,要么是完全可扩展性,例如Petri网4[19]或仅允许一个级别的组件结构,例如(定时)自动机方法,如UPPAAL [3]。(iv) 结果解释认知和界面规范的复杂性使得很难以用户/设计师友好的方式解释组合行为。 如果所选规格不符合以下条件,则情况尤其如此:操作本质上是形式化的,这将是本文中的情况,并且用户/设计者不是形式化方法专家。为了解决这个问题,需要系统地隐藏规范的部分的技术。因此,使得仅与特定分析相关的行为点可见。LOTOS。本文并不声称所有这些要求都可以完全实现与目前的研究状态,而是努力使他们的实现一个不平凡的贡献。在这方面,我们的建议是使用一个过程演算的syndetic建模符号。从过程演算规范中,我们选择了LOTOS [4],因为它在HCI建模中得到了相对广泛的应用。然而,它在认知行为建模中的应用是新的。选择LOTOS(以及一般的过程演算)的原因有很多,参见示例[5];这里我们集中讨论它如何满足刚才强调的联合建模的四个要求。事实上,本文的主体将根据这些需求中的每一个进行结构化,每个部分都解释了我们基于LOTOS的方法如何解决特定的需求。然而,重要的是要注意,这里的讨论来自于大量关于使用LOTOS来建模认知行为的工作,这些工作在[5,7]中有4虽然层次Petri网在一定程度上解决了这个问题。100此外,对LOTOS进行全面介绍超出了本文的范围。因此,假设有一定的符号知识。此外,在整个文件中,我们使用减少LOTOS符号,以简化演示。例如,流程定义中不包括门列表ICS。所选择的认知模型是相互作用认知子系统(ICS)[1]。[2]认为HCI中通常采用的认知理论,例如GOMS系列模型,是针对低层次的分析,以及具体的认知功能,如预测特定任务的执行时间,因此它们的范围有限。相比之下,ICS试图提供一个“统一的”通用认知框架,当在交互丰富的环境中建模时,这种广泛的范围是至关重要的;例如多模态界面。 此外,还有以前的工作,例如[10,9]在HCI中应用ICS,我们将以此为基础。纸的结构。在下一节(2)中,我们对ICS进行了非常概括的介绍。然后,在第3、4、5和6节中,我们讨论了刚才介绍的联合建模的四个要求,依次讨论了LOTOS如何满足每个要求。第7节从方法论上演示了如何使用LOTOS来分析多模态用户界面的可用性,最后,第8节给出了结论性意见。2交互认知子系统我们现在对ICS进行一个非常简短的回顾,以完整介绍感兴趣的读者可以参考[1]。信息流和表述。ICS中的基本这个术语包括所有形式的心理代码,从视觉感官系统中发现的“形状和颜色的模式”到语义子系统中发现的“语义空间中实体和关系的描述”。 我们假设一组Rep表示,其中包含空元素,表示为空。这些表示在体系结构的组件之间传递,在每个组件中从一个代码转换为另一个代码。因此,架构可以被看作是一个信息流模型。子系统。架构的组件称为子系统,所有子系统都具有相同的通用格式,如图1所示。每个子系统本身都包含组件。 例如,由子系统接收的表示被存储在输入阵列中。每个子系统都包含一组转换,这些转换从输入数组中获取表示,对其应用一些转换操作,然后将新的(转换后的)表示中继到目标子系统。我们在这里不考虑图像记录,参见[5]进行讨论。101MPL从商店图像记录来存储输入代码C输入阵列副本变换C到X变换C到Y变换C到ZFig. 1. 通用ICS子系统格式mpl_prop_mplobj_mplprop_objobj_prop眼睛视力视觉对象图二. 阅读配置建筑。我们没有展示完整的ICS架构,这在本文的范围内是很难理解的,我们专注于架构的特定配置-阅读配置,如图2所示。每个子系统都是刚刚突出显示的一般子系统格式的特殊化。所示子系统的作用如下:• 视觉(VIS)-从眼睛接收编码“形状和颜色模式”的表示• Morphonolexical(MPL)-对声音空间中的实体和关系进行抽象的结构描述,即单词的词汇身份,它们的状态和顺序;• 对象(OBJ)-与视觉空间中的实体和关系的抽象结构描述一起工作,例如对象的属性:形状和相对位置;• 命题(PROP)-与语义空间中的实体和关系的描述一起工作,即为实体提供语义含义并突出显示OBJ道具VIS102实体之间的语义关系子系统之间可能的转换如图2所示。多个流和混合。表示流的源通常是感觉子系统,例如VIS。每个表示然后通过变换5的发生在架构内被中继。架构中可以同时存在多个数据流。当收到多个数据流时,该体系结构可容纳许多不同的结果然而,有趣的是,如果输出变换作用于作为两个(或更多个)“竞争”输入表示的组合的表示。这种可能性导致了混合的概念。来自不同视图的表示可以混合以创建复合表示。然而,混合的性质取决于所考虑的齿轮任务。例如,只有当两个表示在某种适当的意义上是一致的时,混合才可能。3一般规范原则在这里,我们考虑两个问题,完全一般的结构和相互作用的原则。3.1结构化软件系统的规范化构造的一种常见方法是使用抽象的定义良好的结构,将系统组件的描述打包成可用作构建块的单元。在软件开发领域,这导致了结构化原则,如Z中的模式,过程,模块和类。LOTOS中的主要结构化构造是过程。流程是一个自治的、并发演化的实体。每个进程都包含许多交互点,在这些点上它可以与其环境进行通信,即与其他并发演进的进程进行通信。我们认为一个过程的概念作为一个适当的一般结构范式,以基础联合建模。认知结构和界面的基本组成部分都可以被建模为LOTOS过程(见3.3小节),5实际上,关于如何通过建筑物传达陈述,存在着一场辩论结构。在这里,我们假设离散变换点火。对于我们的目的来说,这是一个合理的抽象。1033.2相互作用显然,在一个由自治组件构建的模型中,需要提供一种机制,使组件能够进行交互。此外,委员会认为,如果我们选择的符号是合适的,那么这种交互范例必须足够原始,以在接口和认知域中支持组件间通信。我们相信过程演算交互范例是非常原始的。进程演算中的进程通过执行同步的rendez-vous/handshake进行交互当两个进程都准备好时,发生原子6这样的原始交互产生了动作的过程演算概念。这种交互范式的原始性质可以从以下观察中看出:更复杂的交互机制(如异步或共享内存通信)可以从基于动作的交互中构建,因此可以被视为派生行为[14,17]。此外,在认知域中的交互可以使用同步的rendezvous构建ICS中的交互是基于转换职业的。这些事件在LOTOS解释中被建模为动作执行。例如,操作实例,vis obj?r:代表在转换vis obj上对从VIS接收表示(将绑定到变量r)的OBJ子系统进行建模。3.3图示作为说明,我们提供了以下基于交互器的接口和LOTOS中ICS描述的示例:• 接口交互器。 对于交互式软件的结构化描述,已经开发了交互器模型[12,15]。交互器模型形成了一个抽象的框架,用于描述交互系统中的组件。通过将基本交互器模型嵌入到特定的语言或建模方法中,LOTOS交互器模型(LIM)描述了LOTOS中的交互器行为。它组织用于描述系统行为的动作沿着三个维度:动作类型(控制或信息),发起者(应用程序或用户端)和方向(输入和输出)。互动器被认为是一个实体,能够调解用户和应用侧。它对用户生成的输入提供反馈,并使用[6]这种原子性的假设很重要,因为它证明了并发的交错解释是合理的,这是进程演算方法的核心。例如,模拟工具是基于交错的。104侧输出接收输入发送应用侧输出发送输入接收 用户图三. 交互器外部视图触发事件以指示进一步的输入和输出。图3给出了LIM-交互器的外部视图。它显示了与用户和界面的应用程序端的通信以及输入和输出的触发器LIM-interactor的内部视图如图4所示。该结构基于计算机图形参考模型,但由LIM交互器处理的信息不需要是图形的。交互器由四个(子)过程组成。在集合中,信息的抽象表示被保存,并由交互器操作和表示。表示部分在集合被触发时获取抽象表示。它使用这种表示来使信息感知到用户或将其传递给较低级别的交互器。在测量组件中,收集来自用户的输入。当这个组件被触发时,它将输入传递给抽象组件,在那里它被转换为抽象表示,可以传递给应用程序或更高级别的交互器。下面是一个LIM交互器的例子,它对通用逻辑输入设备(LID)的行为进行建模[11]。M:= im1; me; M [].[]imj; me; M[]it1;mc; M[] .[]itm;mc; MP:=me;eo;PA:=mc;od;ALID被指定为测量(M)、呈现(P)和抽象(A)组件的并行组合,这些组件都被指定为LOTOS过程。动作im1至imj对测量过程接收的输入进行动作it1到itj对输入触发器进行建模。动作mo是表示发送的输出,od是抽象过程生成的输出然后,将LID指定为上述过程输出触发输入触发105输出触发UCMC输入触发我测量呈现抽象收集输出接收输入发送输出发送输入接收uc:更新集合,me:测量回显,mc:测量控制见图4。与me和mc适当同步的interactor的内部视图隐藏:LID:= hide me,mc in((P||| A)、|[me,mc]|M)• ICS。 所有ICS子系统具有相同的通用格式,如图所示1. 因此,LOTOS子系统描述也有通用格式。例如,OBJ子系统将被定义为:OBJ(iA:inArr,.):=( vis_obj?r1:Rep; exit(...)||| prop_obj?r2:Rep;exit(.)(* 输入端口 *)|||( obj_mpl!transOM(get(iA)); exit(..)|||obj_prop!transOP(get(i));exit(.)||| obj_lim!transOL(get(iA));exit(..))(* 输出端口 *))>> accept r1,r2:Rep in OBJ(#(r1,r2,0,0),.)其使用数据结构iA来对输入数组7进行建模;get和transON是分别从输入数组中获取和转换相关元素的数据操作;以及>>是顺序组合。因此,子系统独立地执行所有五个转换(两个输入,vis obj和propobj,以及三个输出,objmpl,objprop和objlim),然后递归(通过顺序组合),更新输入数组个资料时假设我们有所有子系统的过程定义,我们可以使用并行组合来构建ICS的顶级行为。作为一个示例,图2中所示的读取配置可以使用以下顶级7实际上,还有其他数据结构,这超出了本文的范围,discuss.106子系统组成((VIS(...)|[vis_obj]| OBJ(.))的方式|[obj_prop,prop_obj]|PROP(...))的方式|[obj_mpl,prop_mpl,mpl_prop]| MPL(.)4对认知行为的不完全理解为了解决认知行为只能部分解释的问题,必须确定描述认知模型的适当抽象层次。我们相信,进程演算提供的抽象技术有助于实现这样一个层次的规范。有一系列可用的建模技术,参见图5,两个极端是基于编程的方法,例如通常用于实现认知模型的方法,例如LISP程序时间逻辑8.前一种方法的弱点是,它们往往过于规范,对认知模型的一种特殊的“机械”解释,使人们不清楚程序行为的哪个方面是认知模型的结果,哪个方面是执行决策的结果。从形式上讲,程序只是一个单一的实现.相反,抽象逻辑技术可以描述一组可能的实现。因此,实现了对实现细节没有规定性的规范。然而,逻辑描述通常表示整个系统的全局属性。因此,这样的方法通常不能反映被建模的系统的底层组件结构。此外,它们通常无法支持规范的执行,即使是以模拟的形式。可以看到过程结石位于这两个极端之间,见图5。首先,我们给出的LOTOS规范肯定反映了ICS模型的组件结构,例如,我们为每个ICS子系统提供了LOTOS过程。这使得规范更容易理解和维护。先前基于模态动作逻辑[10,9]的ICS描述并没有直接反映这种组件结构。其次,它们使用LOLA和Smile等工具实现模拟执行[16]。第三,过程演算提供了避免过度描述的技术。特别是,它们通过允许定义包含非决定论来促进松散的规范。非确定性作为并发的副产品自然地出现在进程演算然而,此外,非决定论可以用来避免对[8]请注意,这里我们并不是指逻辑编程方法,而是指纯粹的抽象逻辑,与Prolog相反,它不包含数据的框架107更抽象进程演算结构化更像是实现图五、可用建模技术的范围性能.具体地说,许多可能的行为可以包括在同一规范中,它们之间的选择是未指定的。此外,非决定论具有非常好的数学性质。例如,在一个示例中,对于一个大类的性质,任何这样的性质,保持在一个规格S也将保持在任何规格,是这意味着我们可以证明的关于抽象(即非确定性)规范的任何此类性质也将适用于任何更具体(即更具确定性)的规范。作为一个例子,我们可以定义一个层次的解释混合。例如,假设objprop作用于表示r1的混合和r2(已从VIS和PROP放入OBJ输入数组中),见图6。有许多可能的方法来生成新的表示r:(i) r∈Rep,即r从所有表示的集合中随机选择(ii) r = r1 r = r2,即 r是r1和r2的随机选择;(iii) cons(r1,r2)=comp(r1,r2),<$cons(r1,r2)<$r=null如果r1和r2是基于非结构化逻辑的方法编程解决方案108123OBJR1obj_propRR2见图6。共混更确定性的见图7。 非决定论的层次因此,1.是最不确定的解决方案,如图7所示请注意,虽然极端的非决定论固有的1。使得解在认知上是奇怪的,即R与R1或R2没有关系,这仍然是分析上有用的解释。具体地说,对于许多认知性质的分析,我们将只对(或可能只需要对)发生在某些子系统上的混合感兴趣,我们可以完全不具体化所有其他混合,即。我们不关心选择什么样的代表5扩展性LOTOS能够以组合和分层的方式构建大型系统规范。• 组合性。LOTOS并行运算器,|[G]|,是一种强大的组合。新的行为可以在不破坏现有流程的封装的情况下逐步添加。 此外,该操作符既可以在结构上使用(即添加目标系统中的组件),也可以在结合上使用(即以逻辑结合的方式添加“全局”约束)。后一种可能性产生了所谓的约束导向的规范风格,这被认为是LOTOS的主要好处• 等级森严。进程本身可以包含进程,因此可以包含并发行为。作为这种并发层次结构的联合建模说明。我们可以将联合分析的顶级行为描述为:109接口(.)|ICS(.)|ICS(...)其中两个组成过程可以在第3节中所示的风格中定义,每个过程都包含并发行为,G是接口和ICS之间的公共动作集,例如通过lim handICS转换直接(或间接)6结果解释过程演算提供了一套强大的工具来分析和解释规范。• 压实。首先,接口和认知架构的完整规范的复杂性可以通过LOTOS隐藏算子以某种方式隐藏起来。这允许对环境隐藏一组操作。因此,如果可以识别与特定分析相关的一组动作,则可以隐藏所有其他动作。例如,如果我们有兴趣仅在ICS的感觉和发射器端口观察/分析ICS的行为,则可以通过隐藏所有其他动作来做到这一点,这里是动作G的集合,即,在ICS中隐藏G此外,包含内部行为的状态空间可以通过应用等价性来减少,例如弱互模拟和测试等价性[14,17]。这些等价关系所涉及的规范在某种适当的意义上是外部观察者无法区分的。重要的是,不可分辨的特性可能具有非常不同的内部行为,其内部复杂性水平可能会有很大的差异• 分析. 在联合建模的背景下,可以采用许多可用的过程结石分析技术。我们列出三种技术。(i) 模拟处决。 诸如LOLA和Smile [16]之类的工具使规范能够在仿真环境中执行。方法是运行指定,工具的用户交互式地解决选择和非确定性(也可以自动解决此类分支)。模拟执行可以与内部动作压缩相结合,只需观察特定交互点的行为。(ii) 验证可以使用测试和模型检查等工具来自动确定syndetic specification是否满足某些属性。使用测试时,属性被编码为测试进程然后对规格进行分析,看它是否会通过测试。通过模型检查,属性在时序逻辑中编码,然后模型检查器自动分析syndetic specification是否满足属性。110(iii) 逻辑演绎。 虽然功能强大,但模拟执行和验证技术并不能在所有情况下都适用。例如,当考虑无限状态空间系统的性质时,通常需要演绎推理。这可以在使用这种演算的公理化的过程演算中或在相关逻辑中执行。7完整架构[5]描述了一个规范,然后在一些认知属性的背景下分析ICS不幸的是,这超出了本文的范围,以充分描述这一机构的工作,但我们总结它在这里。• LOTOS规范。 使用本文前几节中强调的原则,给出了ICS的LOTOS规范。从语义上讲,LOTOS规范可以解释为一组状态序列,称为间隔。这些区间中的状态包含一个可区分的变量,该变量指示在该状态处发生的动作。因此,在执行动作时进入新的状态。我们用(P)表示P的区间。• 目标制定逻辑。 我们引入了一个时间间隔逻辑,它可以用来制定ICS的认知属性。这是基于[6]中描述的逻辑Mexitl。这个逻辑是在最后一个要点中描述的时间间隔内解释的。这样,我们就在LOTOS和区间时态逻辑之间建立了语义联系。• 案例研究。我们分析了ICS执行某些多模态任务的能力。这些任务源于MATIC系统的评估例如,我们分析的一个典型的负属性是:(r1/=r2)国际中心|=<$a(s峰值(r1)峰值(r2))其中,ICS是ICS的LOTOS规范; S| = φ表示S满足公式φ;ri是表示,并且在一个区间上成立,该区间包含一个子区间,在该子区间上成立。非正式地说,这个属性声明不可能在“同一”时间说出一个表示并定位(即用鼠标指向)不同的表示9一个典型的积极属性是:(<$r)(<$σ∈<$(ICS))σa(speak(r)alocated(r))[9]实际上,这里使用不同的表示法有点微妙,更准确地说是r1r2表示不同心理主体的表征111其非正式地声明可以在“相同”时间讲话和定位相同的表示• 分析. 模拟和演绎推理是用来进行这一分析。具体地,我们使用区间时态逻辑中的演绎推理来验证上述否定性质的形式的性质。这种推理使用了逻辑的公理化。相比之下,使用模拟工具LOLA建设性地验证了正特性。因此,一个完整的跟踪是通过模拟执行规范交互式地构造的。8结论我们鼓励在联合建模中使用LOTOS。LOTOS以前曾被用于人机界面的建模。然而,我们使用符号来建模认知行为是新的。 此外,本发明还提供了一种方法,我们相信LOTOS提供了一个有趣的替代模态动作逻辑,它通常用于联合建模[10,9]。我们对LOTOS的主要偏好是,我们相信它为集成接口和认知规范和分析提供了适当的抽象级别,因为它位于规定性(编程)和非常抽象(逻辑)的建模符号之间。更广泛地说,我们认为,这种练习在应用正式的方法来描述和分析认知和人机交互模型具有很大的潜力。特别是,这种技术提供的抽象层次似乎直观地适合这种分析。确认这里介绍的工作是在TMR TACIT项目(由欧盟根据TMR方案,合同N. ERBFMRXCT970133),因此,我们必须感谢该项目的所有成员。我们特别要感谢大卫·杜克、大卫·杜斯、乔恩·梅和菲尔·巴纳德,我们与他们进行了宝贵的讨论。引用[1] PJ巴纳德交互式认知子系统:用多处理器架构建模工作记忆现象。以.Miyake和P. Shah,编辑,工作记忆模型。剑桥大学出版社,1998年。[2] P.J.巴纳德和J.梅。代表复杂任务中的认知活动。人机交互,14(1/2):93[3] 作者:John Bengtsson,Kim G.拉尔森,弗雷德里克拉尔森,保罗彼得斯的儿子和王毅。Uppaal -实时系统自动验证的工具套件。112第四届DIMACS混合系统验证与控制研讨会论文集,1995年。[4] T. Bolognesi和E.布林克斯玛介绍ISO规范语言LOTOS。Comp. Networks andISDN Systems,14(1):25[5] H. 鲍曼认知理论在共现理论中的诠释(长版)。技术报告8-98,计算实验室,肯特大学坎特伯雷分校,1998年。http://www.cs.ukc.ac.uk/pubs/1998/646/index.local。[6] H. Bowman,H. Cameron,P. King,and S.汤普森使用区间时序逻辑的结构化多媒体文档的规范和原型。在Int. Conf. on Temporal Logic,AppliedLogic Series. Kluwer,1997年7月。[7] H. Bowman和G.法孔蒂使用lotos和mexitl分析认知行为。Formal Aspects ofComputing,11:132[8] D. Duke,G. Faconti和M. 马辛克同步和延迟 用户认知的正式模型。In S.Constantine , editor , Proceedings of the ERCIM Workshop on UserInterfacesforAll , Prague , 1996.http://www.ics.forth.gr/ercim-wg-ui4all/UI4ALL-96/proceedings.html。[9] D.J.杜克,P.J.巴纳德,D.A.杜斯和J.梅。联合建模。Human ComputerInteraction,13(4):337 - 3 9 3 , 1 9 9 8 .[10] D.J.杜克P.J.巴纳德J.梅和D.A.杜斯人机界面的系统开发1995年在布里斯班举行的第二届亚太软件工程会议。IEEE计算机协会出版社,1995年12月。[11] G. Faconti,A. Fornari和N.扎尼形式规范的视觉表示:层次逻辑输入设备的应用。专注于计算机图形学系列。Springer-Verlag,1994.[12] G. Faconti和F.帕特诺一种对相互作用的组成部分进行形式化描述的方法。在90年代的欧洲制图中北荷兰,1990年。[13] FM在其他地方2000年,《其他地方的正式方法》(Formal MethodsElsewhere)。http://www.cs.ukc.ac.uk/people/staff/hb5/Elsewhere。[14] C. A. R. 霍尔通信顺序进程。普伦蒂斯·霍尔1985年[15] ISO/IEC。计算机图形参考模型。国际标准化组织,1992年。ISO/IEC11072。[16] LOTOSPHERE。LOTOS集成工具环境。LOTOSPHERE项目,1988年。http://wwwtios.cs.utwente.nl/lotos/lite/。[17] R.米尔纳 通信和并发。 普伦蒂斯-霍尔,1989年。[18] L.尼盖和J·库塔兹。应对多式联运挑战的通用平台。在ACM CHI'95的会议记录ACM Press,1995.[19] W. Reisig. Petri Nets,An Introduction。 Springer-Verlag,1982.
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- Simulink在电机控制仿真中的应用
- 电子警察:功能、结构与抓拍原理详解
- TESSY 4.1 英文用户手册:Razorcat Development GmbH
- 5V12V直流稳压电源设计及其实现
- 江西建工四建来宾市消防支队高支模施工方案
- 三维建模教程:创建足球模型
- 宏福苑南二区公寓楼施工组织设计
- 福建外运集团信息化建设技术方案:网络与业务平台设计
- 打造理想工作环境:详尽的6S推行指南
- 阿里巴巴数据中台建设与实践
- 欧姆龙CP1H PLC操作手册:SYSMACCP系列详解
- 中国移动统一DPI设备技术规范:LTE数据合成服务器关键功能详解
- 高校竞赛信息管理系统:软件设计与体系详解
- 面向对象设计:准则、启发规则与系统分解
- 程序设计基础与算法解析
- 算法与程序设计基础概览
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功