没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记160(2006)57-73www.elsevier.com/locate/entcs基于着色Petri网的软件构件形式语义Remi Bastide和Eric Barboni1,2LIIHS-IRIT法国图卢兹第一摘要本文提出了一种基于着色Petri网的构件模型,该模型既符合软件工程的实际,又具有良好的形式语义。 我们的建议结构如下:1)定义一个组件模型。我们选择了受CORBA启发的组件模型组件模型(CCM),但更简单,更精确。2)提出一种符号来正式指定软件组件的内部行为。我们的正式方法是基于有色Petri网,这使得它非常适合于并发,分布式或事件驱动系统的建模,并服从正式验证。3)从组件模型的构造(面,容器,事件源和汇)到基于Petri网的行为规范的构造(例如,位置,转换等)。4)提供组件间通信原语的正式定义,(调用方法、基于事件的通信)。 这个定义也是用Petri网给出的。 5)提供组件集合的指称语义,以定义此类系统的行为根据每个组件的单独行为和组件间通信原语的正式定义。这种方法的预期好处是三方面的:1)更方便的符号来描述并发和分布式软件组件的内部行为,2)提供组件功能(如事件多播或服务调用)的正式,明确的语义,3)并且,与前面的这两个是必要条件,或者是一些方法来推理用这种方法设计的组件的组件,特别是在数学上验证它们的属性保留字:构件模型,着色Petri网,信号网1介绍目前,工业软件组件模型领域的主要竞争者似乎是Microsoft .Net框架[14],基于Java的组件,如JavaBean [4]和CORBA组件模型(CCM)[16]。 虽然他们在细节上分歧很大,但他们已经确定了一个共同的核心概念,这表明该领域已经达到了一定的成熟度。这些共同的概念是:1电子邮件地址:bastide@irit.fr2电子邮件:barboni@irit.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2006.05.01658R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57• 将组件视为通过公开的软件接口访问的黑盒。这些接口定义了组件执行的合约• 提供多播、基于事件的通信以及单播方法调用,• 提供组件的设计时组装和配置,特别是,• 通过暴露的属性对组件进行设计时配置。基于可重用性的编程的出现主要归功于软件行业,该行业关注于提高软件产品的可重用性。 它已经成为一个商业市场。 我们做了大量的工作涉及工业环境中的实际可用性问题,例如部署设施。更少的工作是提前投入到基于组件的编程的形式和理论基础。研究界见证了基于组件的编程在工业上的成功,在过去的几年里已经开始投入大量的活动来奠定这样的基础[11,5]。本文提出了一种构件的形式化模型,特别是旨在为上述软件构件的主要概念提供一个形式化的语义框架。为此,我们定义了五个步骤:• 定义组件模型。我们选择了一个受CORBA组件模型(CCM)启发的组件模型(特别是,我们重用CCM词汇表用于组件的功能),但更简单,更精确。我们工作的重点是组件活动的行为语义,并忽略了CCM的许多实际方面(如部署),这些方面在工业环境中是基本的,但主要是诉诸垂直和传达很少的理论兴趣。• 提出一种符号来正式指定软件组件的内部行为。我们的形式化方法基于着色Petri网[7],着色Petri网是一种众所周知的、广泛使用的和工具支持的符号,并建立在我们以前关于CORBA对象的形式化规范的工作[1,2]上。它可以被认为是以前面向对象的工作到面向组件的编程的扩展。它的Petri网基础使其特别适合于并发、分布式或事件驱动系统的建模[12],并适合于形式验证。• 定义一个从组件模型的构造(例如,刻面、容器、事件源和汇)到我们基于Petri网的行为形式主义的构造(例如,位置、过渡等)。• 提供组件间通信原语的正式定义(方法调用,基于事件的通信)。这个定义也是用Petri网给出的。• 提供组件集合的指称语义,以便根据每个组件的单独行为来定义此类系统的行为R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)5759组件和组件间通信规范的正式定义。虽然用于指定组件行为的符号这种方法的预期好处有三个方面:• 除了描述并发和分布式组件的内部行为的方便符号外,• 为组件特性(如事件多播或属性,特别是组件间通信)提供正式的、明确的语义,• 而且,前两个是必要条件,或者有一些方法来推理用这种方法设计的组件的装配,特别是在数学上验证它们的属性本文件的结构如下:我们首先描述我们的组件模型及其可视化表示。 还描述了组件组装的概念。然后,我们提出了一个简单的案例研究,将用于整个文件来验证我们的方法。 的情况首先是以组件组装的形式进行非正式描述我们继续描述组件模型和有色Petri网,我们选择的行为符号之间的映射 对于程序集的每个组件,我们都提供了正式的行为规范。最后,我们描述的指称语义,使我们能够自动构建一个单一的,非结构化的信号 从所有组件的行为和它们的相互连接来分析Net。这个网络描述了程序集的整体行为。2CompoNets,我们的组件模型我们的组件模型被称为CompoNets(组件和Petri网的缩写)。它的特性在某种程度上受到了CORBA CCM的启发。特别是,我们遵循CCM理念,将组件所需的功能与它提供给其他组件的功能等同对待。由于我们使用着色Petri网(CPN)来指定组件的行为,因此我们的组件模型的类型系统将以CPN-ML(标准ML的变体)的形式给出。CPN-ML是CPNs的登录语言,本文使用Design-CPN工具来设计模型。CompoNet向外部世界呈现一个由多个端口组成的信封,通过它可以与其他组件进行通信(图1)。端口可以是不同的类别(方面、接收器、事件源和事件接收器)。• 小面:一个小面代表了一组附加到其他组件上的功能特性。每个方面都由一个名称和一个接口来描述,即一组CPN-ML函数签名。 ML语言不支持接口的概念,但我们 在引用其他语言(如Java或CORBA IDL)时使用此术语,60R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57方便地为一组ML函数签名命名• 插座:插座代表CompoNet完成其功能所需的一组功能特性。 插座被描述为类似于用于刻面,通过名称和CPN-ML接口。• 事件源:事件源描述可能由CompoNet发出的事件。 CompoNet对事件源进行编码的事实意味着它将能够将该事件多播到已经表现出他们对该事件的兴趣的一组接收器。在语法上,事件源被描述为无参数CPN-ML函数签名。函数的结果类型可以是任何CPN colourType。特别是,colourType E将经常被使用:在CPN中,E是空颜色类型,用于描述不携带值的令牌。当仅关注事件的发生时,将使用E colourType 。当事件携带某些信息时,专用的CPN-ML colourType(如STRING)将用作描述事件源的ML函数的返回类型• 事件接收器:事件接收器描述CompoNet愿意接收的事件。事件接收器的描述类似于事件源。FacetName:FacetInterfaceEventSinkName:ResultTypeEventSourceName:结果类型ReceptacleName:ReceptacleInterfaceFig. 1. CompoNets的图形语法图1说明了CompoNet的图形语法,给出了用于facet、容器、事件源和事件接收器的图形符号。小平面的图形表示(分别为事件源)和容器(分别为事件接收器)被设计成使得它们可以方便地相互插入为了设计一个系统,设计者将把几个组件组装成一个整体,并连接它们的面和插座(分别)。它们的事件源和事件汇)。• 如果它们具有相同的ML接口,则面可以连接到插座。在一个组件中,一个插座需要连接到一个面:连接描述了哪个组件提供插座接口所描述的功能。相反,面可以连接到零个、一个或多个插座:可以使用面接口描述的特征其他几个组件。• 如果事件源和事件接收器关联的ML函数签名具有相同的结果类型,则可以将事件源连接到事件接收器。事件源可以连接到R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)5761任何数量的事件接收器(从而模拟向多个目的地多播事件),并且事件接收器可以连接到任何数量的事件源(从而模拟组件可以从多于一个源接收相同事件的事实)。3为例为了说明我们的方法,基于组件的建模,我们提出了一个简单的案例研究,从用户界面应用领域。非正式规范所提出的应用程序允许用户将一串文本输入到文本中框中,并通过单击按钮将键入的文本放入未知大小的缓冲器中。相反,另一个按钮允许用户从缓冲器获取字符串,并在另一个文本框中显示检索到的文本。必须根据缓冲器的状态启用或禁用按钮:如果缓冲器已满,则必须禁用Put按钮。相反,如果缓冲器为空,则必须禁用“获取”按钮。图二、案例研究的用户界面部件组件我们运行的示例的用户界面如图2所示,而图3给出了一个组件的组装,为一个可能的软件解决方案建模:图3(左)中的组件显示了在用户界面中也可见的4个可视组件:两个文本字段(PutTextField和GetTextField)和两个按钮(PutButton和GetButton)。它还包含提供应用程序其余行为的非可视组件:MyBu建模器PutAdapter和GetAdapter,它们提供了组装各个部分所需的逻辑。下一节将详细介绍组件中我们提出的组件模型是分层的:一个组件的行为可以给出着色Petri网,或作为其他组件的组装。图3的右边部分表示左边的62R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57不完整空充MyBuffernotEmpty缓冲液:缓enabledisableenabledisablePutButton单击缓冲液:缓冲buffer:缓冲区单击GetButton执行单击执行PutAdapterGetAdapter单击文字:文文字:文文字:文文字:文PutTextFieldGetTextFieldkeyPressed():keyPressed():单击keyPressed():单击图3.第三章。案例研究的组件组装(左)及其层次抽象视图(右)。部分程序集可以像原子组件一样被考虑和使用,参与更高级别的程序集。它公开从其内部组件提升的功能(在本例中,keyPressed事件接收来自PutTextField组件,而click事件接收来自两个按钮。 本文件的重点不是 因此,我们将不给出有关分层组件的技术方面的更多细节。4每个组件的详细规格我们现在继续在图3中给出组件中每个组件的详细规格。这样,我们还将解释第1节中描述的组件模型与我们选择的行为符号着色Petri网之间的映射。GetButton和PutButton组件GetButton组件的信封(图4左侧)显示了三个事件接收器(启用、禁用和单击)事件源和一个事件源(单击)。由于这些事件的返回类型没有指定,因此假设默认的空返回类型为E(严格来说,我们应该写为enable:E,disable:E,click:E)。这个模型的事实,这些事件只是无价值的信号来自或发送到组件GetButton的行为规范如图4(右)所示,它是一个带有几个语法扩展的有色Petri网,其语义将在第5节中正式给出。非正式地,我们可以说,一个按钮接收启用,禁用R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)5763E11`e残疾启用1`e禁用使单击click()图四、GetButton组件的封套(左)和行为(右)和来自其环境的点击信号,并且仅当其被启用时才转发点击信号。Petri网允许正式地陈述这种行为,只要从事件源和事件汇到Petri网中的转换的适当映射被正确定义。事件接收器对于信封中的每个事件接收器,我们将行为网络中的一组转换关联起来。这组转换称为事件接收器的事件处理程序我们选择了一种可视化语法来表示事件处理程序:事件接收器X的事件处理程序中的所有转换在图4(右)中,我们可以看到事件接收器enable的事件处理程序由具有相同名称的单个转换组成,其他两个事件接收器(disable和click)也是如此。这种可视化语法与所有事件处理程序都是不相交的(转换是0或1个事件处理程序的一部分转换属于事件处理程序的事实改变了其通常的触发规则:它成为同步转换。同步转换的概念是由Moalla等人[10]开发的,用于使用Petri网对非自治系统进行建模。 同步转换在启用时不会像其他转换那样自动触发。 为了发射,它需要在启用时从其环境接收信号。非自治系统的概念与基于组件的建模非常相关:每个组件都可能是一个非自治系统,需要来自其环境的输入才能运行。例如,GetButton组件最初是启用的(如图4中 如果在此状态下接收到启用事件,被忽略和丢失:使能转换在此标记中不可触发。但是,接收到禁用事件将使其进入禁用状态,随后的禁用和单击事件将被忽略。请注意,同步转换的概念及其相关的触发规则只是为了让设计人员直观地理解组件64R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57启用1`e已禁用11`eE禁用使单击动态行为:这个概念将不再用于第5节中详细描述的指称语义,并被更一般的信号弧概念所取代事件源GetButton组件只有一个事件源,即click,说明它能够将点击事件发送到其他组件。事件源到Petri网的映射很简单:对于每个事件源S,相同的名称可以用作行为网络中的任何转移T的动作。直观的含义是,当转换T被触发时(因此当T的动作被执行时),事件将被发送到连接到源的每个事件接收器。事件调度函数用于对多播、异步消息发送进行建模。这个直观的意义将在第5节中给出形式化的语义。在我们的GetButton组件中,当点击转换触发时,它的动作会执行并将点击事件发送给所有连接的组件。 请注意,只有在标记了启用位置时,并且外部单击事件发生时,通过点击事件接收器接收。因此,我们有了按钮的预期行为:仅在启用时才发生向前单击事件click()图五、按钮组件的行为PutButton和GetButton具有相同的信封。Put- Button的行为仅与GetButton的行为不同,因为它的初始状态是禁用的. PutButton布局也是不同的,以便于阅读图14- 3中模型的完整语义。MyBuffer组件MyBuffer旨在以面向组件的方式对消息Buffer进行建模。它的包络(图6右)显示了4个事件源(notFull,full,empty,notEmpty)和一个facet(buffer)。[3]严格来说,PutButton和GetButton应该被描述为同一个组件类的两个实例,但代价是MyBu插件中需要一些额外的逻辑来表示其初始状态。 我们选择不这样做是为了让模型更简单。R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)5765接口缓冲区{funput(s:String):E; funget(): String;}图六、Buffer接口(左)和MyBuffer组件Bubcher接口(图6左)是ML函数签名的集合,描述了可以从Bubcher中期望的功能特性。提供了两个服务:put(s:STRING)用于在缓冲器中插入消息,以及get():STRING从服务器获取消息。与此组件相关联的行为规范旨在描述这些服务何时可用,以及它们对组件状态的为了简单起见,我们选择了一个非常简单的单槽缓冲器模型。此缓冲器最多只能包含一条消息,因此要么为空,要么为满。尽管它很简单,但它完全符合图6右侧所示的信封。这个组件将允许我们说明从刻面到Petri网的映射。面的映射组件封装中的facet F是一组ML函数签名。对于这个集合中的每个签名S,在行为网络中定义了两个同名的位置:• 一个称为服务输入端口(SIP)的地方。以图形方式描述了SIP在网络上的一个注释。SIP旨在对组件中服务调用的到达进行建模。• 一个称为S的服务输出端口(SOP)的地方。从图形上看,SOP由网络中的[out]注释描述。SOP旨在对组件中服务调用的结果进行SIP和SOP的令牌类型是从签名S的参数推导出来的:例如,place [In] put的令牌类型是STRING,而place [Out] put的令牌类型是E(空令牌类型),因为put服务的签名是fun put(s:String):E. SIP在行为网络中只能有输出弧。相反,SOP只能有输入弧。有了事件源和facet的映射,我们可以用有色Petri网来指定MyBu插件的行为(图7)。初始标记表明缓冲器在其消息位置中最初具有消息,因此是满的。组件可以随时接收put和get调用,这将66R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57SS消息11“你好”放插入出来得到提取物在roomLeftgetString();void run();字符串1`initialMessage字符串图7.第一次会议。MyBu插件组件的行为规范导致在相应的SIP中接收到令牌。 如果接收到一个put调用, 在这个初始状态下,插入转换是不启用的,因此令牌将停留在[In] put位置,直到接收到对get的调用、处理并导致令牌被存放在roomLeft位置。从这个标记,插入转换可以触发,将结果令牌存放在[Out] put位置。图7还利用了上述事件源的映射。例如,当提取转换触发时,它会发出notFull事件(因为 缓冲器不再满)和事件空(因为它现在是空的)。PutTextField和GetTextField组件PutTextField和GetTextField是同一个组件类的两个实例:它们具有完全相同的信封和行为。接口文本{fun setText(s:String); fun getText():String;}图8.第八条。Text接口(左)和PutTextField组件Text界面(图8左侧)列出了 text组件:一个服务(setText)用于设置文本区域的内容,一个服务(getText)用于检索其内容。像PutTextField(图8右)这样的文本区域支持这个方面,并且有一个事件接收器keyPressed,允许通过某种形式的用户界面交互来交互式地更改文本内容两个文本字段的行为如图9所示。 文本字段的初始内容是空字符串,可以通过调用S字符串放在S得出来R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)5767S字符串getText出来getTextsetText STRINGInt1“”字符串Ss内容不SMcombine(m,keyPressed按键getText在图9.第九条。PutTextField和GetTextField组件的行为setText服务,或者通过keyPressed事件交互式地编辑字段的内容。我们假设存在一个combine(text:STRING,char:STRING):STRING ML函数,它允许在字段的内容中添加字符GetAdapter和PutAdapter我们通过给出行为来完成案例研究的正式规范,GetAdapter和PutAdapter组件,这将引导我们详细介绍尚未遇到的插座映射。这两个适配器组件用于使按钮触发的事件适应MyBu插件和两个文本字段提供的服务。在事件驱动的编程库(如用于基于Java的用户界面的Swing库)中,经常需要这样的适配器类E1 `e输出动作执行准备11`elet val result = buffer.get()in(s)端s文本字符串SsetTextactiontext.setText(s) end图10个。GetAdapter组件的封套(左)和行为(右)插座映射GetAdapter组件(图10左侧)有两个插座:setText出来setText68R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57• buffer,与图6(左)中给出的接口Buffer相关联。这模拟了GetAdapter将使用另一个具有Buffer facet特性的组件提供的服务的事实。• text,与图8(左)中给出的接口Text相关联。这模拟了GetAdapter将使用另一个具有Text facet的组件提供的服务的事实。在组件的包络中存在容器R使得能够在组件的行为网络中定义特殊的调用转换。调用转换是一种转换,其动作具有特殊的形式receptacle-- Name.serviceName(parameters),其中serviceName是receptacle接口中的函数之一。调用转换对另一个组件上的方法的单播同步调用进行建模,这与由事件源建模的异步多播事件分派相反。同样,这种调用转换的形式语义将在后面详细介绍(第5节)。在GetAdapter组件的情况下,我们有两个这样的调用转换:perform转换调用buffer容器上的get()服务,setText转换调用文本容器上的setText()服务。 前者也在执行事件接收器上同步。在自然语言中,我们可以说当GetAdapter组件接收到一个执行事件时,它首先通过调用buffer.get()从buffer获取一条消息,然后通过调用text.setText()在文本字段中显示结果消息。 这种行为正是 在图10(右)的行为网络中进行了正式描述输出动作执行E准备1`e11`elet val result = text.getText()in(s)端s文本字符串S放actionbuffer.put(s)end见图11。 PutAdapter组件的封套(左)和行为(右)。PutAdapter的envelope与getAdapter的envelope相同,其行为也非常相似:唯一的区别是调用transitions的action中调用的方法:当PutAdapter接收到一个执行信号时,它通过调用text.getText()来检索其文本字段的内容,并通过调用buffer.put()将此字符串插入buffer中。R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57695指称语义到目前为止,我们已经展示了如何着色Petri网可以用来模拟软件组件的行为,具有同步单播方法调用和异步多播事件调度。这种描述需要几个语法扩展到传统的彩色PN(服务输入/输出端口,调用转换,同步事件处理程序转换和事件调度功能)。剩下要做的是给这些句法扩展一个形式语义。这种形式语义将以指称的方式给出。根据B. Meyer [9],(源)语言的指称语义通过翻译方案表达程序的含义,对于(源)语言的每个程序,翻译方案产生更简单(目标)语言的程序.对我们来说,源语言是组件及其行为网的组装,目标语言是信号网,这是Starke和Roch开发并广泛研究的有色Petri网的变体[15]。在 下 文 中 , 我 们 将 首 先 介 绍 用 于 为 facet/receptacle 连 接 器 和 event-source/event-sink连接器提供指称语义的Petri网模式,作为示例,我们将在附录中给出作为汇编的正式指称语义的信号网(图14)。面/插座连接器Facet/receptacle连接器用于对两个组件之间的方法调用进行建模。和面向对象语言一样,我们组件模型中的方法调用是单播的(调用的客户端或发射器必须知道一个服务器或接收器)和同步的:客户端等待来自服务器的结果。这样的通信模式很容易用Petri网建模:早在1980年,Ramamoorthy [13]就描述了典型的客户机/服务器通信Petri网模式。我们在[1]中详细描述了这种模式在分布式对象系统建模中我们重用这个模式,并扩展它来正确处理高级Petri网和并发调用,如下所示:• 调用转换仅存在于至少具有容器的组件中。行为网中的每一个调用变迁都被看作是一个宏变迁,由请求变迁、等待位置和结果变迁依次连接而成。请求转换通过输出弧连接到拥有连接面的组件的行为网络中的对应服务的服务输入端口(SIP)。 相反,服务输出端口通过输出弧连接到结果过渡。• 尽管在我们的简单案例研究中没有出现这种情况,但我们必须正确处理潜在的并发调用。同一个服务可以被多个组件并发调用,可能使用不同的参数。我们需要70R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57一种适当的结构,以确保服务的结果返回给适当的客户端。为此,我们定义了一种名为INVOCATION的新颜色,用于标识每次调用。请求转换通过调用ML函数gensym()生成新的INVOCATION值,该函数在每次调用时返回不同的值。 该值被附加到SIP、SOP和等待位置中的令牌。 因此,着色Petri网的统一机制确保了正确的客户端获得调用的结果。E11'E1'E准备好了getText在return(i);行动let val invocation = gensym()in(i)端我调用SIgetTextS(m,keyPressed())output(i);actionSTRINGParamSTRINGParam字符串let val invocation = gensym()in(i)端见图12。小面/插座连接器标记模式。图12 举例说明了客户端/服务器通信的 Petri 网模式。该图显示(部分)PutTextField的行为网络(左),PutAdapter的扩展网络(中)和(部分)MyBu插件的网络(右)。PutAdapter中的调用转换已经根据上面描述的模式进行了扩展:例如,我们看到执行转换已经扩展为执行请求,执行等待和执行结果。同样,put转换已经扩展为put request、put wait和put result。保留SIP和SOP库所的[In]和[Out]注释只是为了方便参考原始网:它们不再起作用,库所只是传统的Petri网库所。事件源/事件宿连接器如上所示,组件之间的同步客户机-服务器通信很容易用Petri网来描述。对于异步多播通信,情况就不那么好了。 这种类型的通信甚至可能被证明是特别难以建模的Petri网,这使得斯塔克和Roch定义了一个扩展到彩色PN称为信号网[15]。这是一个真正的Petri网扩展:它已被证明,这种扩展了Petri网的建模能力,图灵机,因此几个调用我放我出来(s(s放在SSS文执行结果(s(sgetText出来我放置等我放置请求卖出结果我执行等待我执行请求插入R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)5771(s放在插入出来得在我提取物属性变得不可判定。然而,有几种分析技术可用于信号网络,并且仍然可以获得有趣的结果,特别是使用模型检查。Signal Nets带来的扩展是信号弧,即连接两个转换的弧。 这种信号弧的语义如下: 信号电弧的目标在其被启用时以及在其从电弧的源转换接收到信号时点火。给出了信号电弧的详细点火规律在[15]中。在我们的例子中,事件调度转换将是信号弧的源,事件处理程序中的转换将是它们的目标。调用s s(s,i)STRINGParam消息字符串11`initialMessage获取字符串图13岁事件源/事件接收器连接器标记模式。图13举例说明了使用信号弧来定义事件源/事件接收器连接器的语义。该图说明了MyBu插件和PutButton组件之间的通信。缓冲器通过触发提取转换来通知它何时为空,通过触发插入转换来通知它何时为满。 这些信号将通过强制目标启用或禁用转换的发生来启用或禁用按钮。信号弧以粗体显示6结论我们已经表明,有色Petri网是一个正式的符号,适合指定单播方法调用以及组播事件调度的软件组件的行为。虽然许多其他研究人员已经使用Petri网来建模基于对象或组件的系统([6,3,8]),但我们相信我们的工作是原创的,因为它定义了一个支持方法和事件的组件模型。为了正确地指定这样的组件,需要几个语法扩展来提供从组件模型的构造到Petri的映射启用E残疾11`e1`e调用E放roomLeft出我禁用使单击1“你好”72R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57net原语。我们已经提供了一个指称的语义,这些语法扩展,给出的信号网,着色Petri网的变体提供了一个非常精确的操作语义。我们的方法的目标是将基于Petri网的规范的好处带到基于组件的建模中。为了真正提供这种好处,还需要做进一步的工作。特别是,由于分析将在由组合中所有行为网络的合并产生的全局网络上执行,因此我们需要研究如何根据设计者已知的原始网络引用[1] 巴斯蒂德河,P. Palanque,O. Sy,D.- H. Le和D. Navarre,基于Petri网的CORBA系统的行为规范,第20届Petri网应用与理论国际会议论文集,Springer-Verlag,1999年,pp. 第66-85页。[2] 巴斯蒂德河,O. Sy,P. Palanque和D. Navarre,CORBA事件服务的形式化规范,第四届开放式基于对象的分布式系统的形式化方法国际会议,2000年,pp. 371-395.[3] Battiston,E.,“用CLOWN建模一个协作开发环境”,OOPMC研讨会,1995年。[4] 英格兰德河, 美国加利福尼亚州塞瓦斯托波尔,1997年。[5] FMCO,www.daimi.au.dk/CPnets/workshop01/[6] Guel fi,N.,O. Biberstein,D. Buchs,E. Canver,M. C. Gaudel,F. von Henke和D.陈文辉,“面向对象的形式化方法的比较”,北京科技大学出版社,2007年。[7] 詹森,K.,着色Petri网《基本概念、分析方法和实际应用》,Springer-Verlag,1997年。[8] 拉科斯角和C.陈文辉,[9] 迈耶湾,[10] Moalla,M.,J. Pulou和J. Sifakis,同步Petri网:描述非自治系统的模型,计算机科学讲义:计算机科学的数学基础,Springer-Verlag,1978,pp. 374-384.[11] 第二届fmco.liacs.nl/fmco03.html[12] 彼得森,J.L.,[13] 拉马穆尔西角V.和G. S.何,使用Petri网的异步并发系统的性能评估,IEEE Trans.软件工程师,1980,pp.440-449[14] Ritcher,J.,“Programming the .NET Platform,” Microsoft Press,[15] Starke,P.和S. Roch,“分析信号网络系统”,技术报告162,Informatik Berichte, 2002[16] Vinoski,S.,CORBA 3.0Commun. ACM,ACM Press,1998,pp.40比52R. Bastide,E.Barboni/Electronic Notes in Theoretical Computer Science 160(2006)57737附件:作为非结构化信号网络的案例研究的指称语义使使EE1`e启用 11`e启用残疾11`e1`e残疾禁用禁用单击输出(i)动作let val invocation = gensym调用调用EE11`e1`e我单击准备卖出结果放roomLeft得到执行请求准备1`e11`e端输出(i)动作出来在我我Elet val invocation = gensym()in(i)端执行请求我我我字符串调用我setTextgetText在放置等待插入提取物执行等待setText_result设置文本输出getText在字符串在SS(s,调用(s,不我11`1“”`”我我我我11”1“”SSS我字符串不(s,(s,setText内容getText执行等待放置请求放消息得到执行结果setText_waitsetText内容getText11 `“hello”1`初始化消息在产出(一)中;输出字符串SScombine(m,keyPressed())(s,i)STRINGParam字符串不SSM(s,S我S我let val invocation = gensym()in(i)端M(s,(s,SS输出(i)动作设置文本输出按键getText出来执行结果文本文本设置文本请求setTextgetText出来在STRINGParam字符串字符串字符串keyPressed()STRINGParamlet val invocation = gensym()in(i)端图十四岁个案研究的指称语义学
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- 电力电子系统建模与控制入门
- SQL数据库基础入门:发展历程与关键概念
- DC/DC变换器动态建模与控制方法解析
- 市***专有云IaaS服务:云主机与数据库解决方案
- 紫鸟数据魔方:跨境电商选品神器,助力爆款打造
- 电力电子技术:DC-DC变换器动态模型与控制
- 视觉与实用并重:跨境电商产品开发的六重价值策略
- VB.NET三层架构下的数据库应用程序开发
- 跨境电商产品开发:关键词策略与用户痛点挖掘
- VC-MFC数据库编程技巧与实现
- 亚马逊新品开发策略:选品与市场研究
- 数据库基础知识:从数据到Visual FoxPro应用
- 计算机专业实习经验与项目总结
- Sparkle家族轻量级加密与哈希:提升IoT设备数据安全性
- SQL数据库期末考试精选题与答案解析
- H3C规模数据融合:技术探讨与应用案例解析
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功