DFC架构中的调用抽象和构件协调

36FMICS 2002初步版本一种支持构件协调的调用抽象帕梅拉·扎维美国新泽西州弗洛勒姆公园ATpamela@research.att.com迈克尔·杰克逊英国伦敦AT T实验室研究中心jacksonma@acm.org摘要DFC是电信服务的组件架构。尽管DFC组件交互所使用的调用协议本质上很简单，但使用它编写有用的组件是相当复杂的。我们诊断问题并提出解决方案，该解决方案采用以高级特定领域编程语言体现的调用抽象的形式。抽象不仅鼓励正确的编程，而且还可以证明组件具有重要的行为属性。1DFC架构电信服务是网络服务，其主要目的是人们之间的实时通信虽然电信服务有125年的历史，但直到20世纪60年代才开始受到软件控制。软件控制导致了功能的爆炸，这导致了复杂性的爆炸，称为功能交互问题[4，7，8，9，14]。分布式特征组合（DFC）架构[12，13，19]是为了解决特征交互问题而开发的。它是一种基于组件的软件体系结构，用于描述和开发电信服务。该模型具有通用性、特征模块化、结构化特征组合和独立于网络的资源DFC是管道和过滤器架构风格的特定于领域的适应[15]。在这种风格中，有一个固定的管道（边）和过滤器图这是一个初步版本。 最终版本将发表在《理论计算机科学电子笔记》上网址：www.elsevier.nl/locate/entcs扎韦和杰克森37（节点）。每个管道都是通用格式的单向数据流。每个过滤器组件都是一个具有完全私有状态的并发进程，它消耗输入流并产生输出流。 因为每个过滤器都是一个上下文无关的模块，所以可以很容易地添加、删除或更改过滤器。DFC有一个称为特征框的过滤器。在管道的地方，它有内部调用。内部呼叫是遵守固定协议的点对点连接，允许在两个方向上传输信号和媒体。每个连接的目的地是在建立连接时确定的，因此特征框和内部调用的图是动态的和自配置的，而不是固定的。尽管存在这些困难，DFC还是采用了与管道和过滤器相同的模块化风格。特征盒表现出透明性，这意味着当它们没有任何事情要做时，它们的存在是不可观察的。他们也有自主权，这意味着他们有足够的权力在没有外部帮助的情况下履行其职能。功能框可以发出、接收或删除内部呼叫。它们可以产生、吸收或传播在内部呼叫的信令信道上传播的信号。它们还可以处理或传输语音或视频等媒体。尽管在DFC方面仍有许多工作要做，但迄今取得的成果令人鼓舞：• 没有已知的电信功能，包括移动和多媒体功能，不能在DFC中描述。这是DFC满足通用性目标的有力证据。• 许多功能的设计（和一些实现）都利用了DFC功能模块化的优势• DFC• 基于DFC的资源独立性，有一种具有许多优点的DFC IP实现2DFC协议及其挑战本文讨论了DFC功能盒所执行的呼叫级信令：在呼叫的信令信道上发起呼叫、接收呼叫、拆除呼叫和交换状态信息。虽然功能盒有其他行为-他们操纵数据和媒体以及调用级信令是盒子程序的第一个和最重要的行为。它是放置数据和媒体操作的框架。DFC内部呼叫的协议相对简单。 内部呼叫由特征盒或接口盒发出，特征盒或接口盒是代表电信设备的持久模块。为了发出呼叫，盒子从端口发送设置信号设置信号到达DFC路由器，DFC路由器决定扎韦和杰克森38基于信号的各个字段，哪个特征或接口盒应该接收呼叫。路由器将信号发送到接收盒的可区分盒端口当接收盒接受呼叫时，它为它选择一个常规端口，并从该接收端口向发送端口发回一个upack信号。这就创建了一个端口到端口的信令通道。在发送或接收upack之后，盒子可以使用呼叫的信令信道来发送它喜欢的任何状态信号。这个信号通道是双向的。在任何方向上，它都是FIFO，并且具有无限的容量。任何一个端口都可以发送一个teardown信号来结束调用;它由来自接收它的端口的downack信号来确认（如果来自两个端口的拆卸信号在传输中交叉，则两个端口都生成下行确认信号。）在端口发送或接收拆除信号后，不允许盒从该端口发送任何后续状态信号尽管相对简单，但我们发现，在实践中，呼叫级信令很难编程，也很难推理。 在与其他组件异步交互并旨在与它们协调以产生有意义的全局行为的分布式组件的上下文中，即使是简单的协议也会变得非常复杂。我们已经诊断了编程挑战，并开发了一个DFC内部调用的抽象，旨在使框编程更容易。抽象体现在用于对DFC特征框进行编程的高级、领域特定的编程语言（名为“Boxtalk”）中。调用抽象的语义是按照普通的有限状态机编写的，Boxtalk中程序的控制框架可以编译到该状态机。DFC盒编程的挑战分为两组。第一组，在第3节中讨论过，包含了当试图让盒子在组件上下文中执行有用功能时出现的复杂性。第二组属性将在第5节中讨论，由每个盒子都应该保证具有的属性组成。 框程序必须组织，使每个属性 可以自动保证，也可以有效地检查。第3节和第5节的每个小节首先介绍主题问题，然后解释由这些问题激发的调用抽象的各个方面。在这两个部分之间是一个更正式的插曲。对于编程示例，我们使用公共交换电话网络中的两个熟悉的功能：呼叫等待和顺序信用卡呼叫。3编程困难3.1港口太低级了在对功能框编程时，引用功能框通过端口名参与的调用是不方便的。这使得无法引用已被拆除的调用，因为端口可能已经分配给了扎韦和杰克森39不同的召唤更重要的是，调用在程序中的角色可以改变，但它的端口不能改变。最常见的例子是呼叫等待（CW）功能。CW功能盒最多可以参与三个呼叫，一个通向其用户，两个通向远方。对于程序员来说，关于两个远端呼叫的最重要的事实是，其中一个连接到订户呼叫，而另一个正在等待（“保持”）。通过端口名来引用这两个调用是很尴尬的，因为它们与哪个调用是活动的，哪个调用是等待的没有任何关系。为了能够以更抽象的方式引用呼叫，每个呼叫在被盒子发出或接收时都被赋予一个内部标识符。该标识符在盒子的生命周期内是唯一的，并且与调用永久关联。一个盒子程序可以声明任意数量的调用变量。每个调用变量的值要么是一个调用标识符，要么是一个区别值noCall（所有调用变量都初始化为noCall）。Box程序通过调用变量引用调用。为了将编程与端口分配完全分离，有必要假设一个盒子可以有无限数量的端口。这意味着当调用需要一个端口时，实现永远不会找不到可用的端口。这个假设在特征框的软件实现中很容易满足。四个Boxtalk语句更改调用变量的值：• 如果建立信号到达，则RCV（c）接收新呼叫。新调用的标识符被分配给调用变量c。• New（C）和CTU（C0，C）发出新呼叫。新调用的标识符被分配给调用变量c。1• 赋值语句（如c1，c2 = c2，-）将调用标识符从一个变量移动到另一个变量。在这个赋值中，c2得到值noCall。右边的变量必须是左边变量的子集，并且任何变量都不能在右边出现超过一次。这些语句保留了一个重要的不变量，即没有两个调用变量指向同一个调用。如果两个调用变量具有相同的值，则它们的值必须为noCall。两 组 调 用 标 识 符 在 语 言 的 语 义 中 占 有 重 要 地 位 。 集 合portAllocated包含当前分配给端口的所有调用的标识符;这些是根据DFC协议当前存在的调用。已知集合是调用变量的值减去noCall的并集。known中的调用对程序来说是可访问的，因为程序1粗略地说，new（c）和ctu（c0，c）之间的区别在于ctu通过调用c0继续一个扩展到这个盒子的管道，而new开始一个新的管道。有关DFC路由算法的细节不在本文讨论范围之内扎韦和杰克森40s_from_subscriber / ctu（s，s？开关接收器s_from_afar /s，a = −，s; cturcv（w）/ s！连续波指示器{src= w.stp.src}w？s？开关/a，w = w，s？开关/a，w = w，是吗？s？tdn /end（a）; a，w =a_from_afar /ctu（a，s）call_waiting：（s，a），w透明：（s，a）all_holded：s，w有一个调用变量来引用它。这些集合经常重叠，但它们实际上是独立的。如果一个调用已被拆除，但其调用变量尚未重新分配给另一个调用，则该调用可以位于known中而不在portAllocated中如果调用变量在调用被拆除之前被重新赋值，则调用可以在portAllocated中而不是在known中（参见3.2节）。设置信号的字段包含有关由它发起的呼叫的重要信息。由盒子接收或发送的每个设置信号都被自动保存，以便程序可以随时引用它。例如，在调用变量c中发起调用的setup信号的src字段的值是c.stp.src。如果一个呼叫在被拆除后仍处于已知状态，则其建立信号仍可访问。图1是呼叫等待功能框的Boxtalk程序。它省略了介质处理，这是不考虑在本文中。除此之外，它是完整的，除了在配套文本部分中给出的一些声明和定义。这种分离允许Boxtalk的图形部分以强调所有重要的呼叫级信令，而不会有太多来自数据操作的混乱。a_from_subscriber /ctu（a，s）{reverse}Fig. 1. 呼叫等待功能框。扎韦和杰克森41从图形上看，程序是一个有四种状态的有限状态机• 初始状态是一个黑色的小圆圈。• 瞬态是一个更大的清晰圆。• 一个稳定的状态是一个矩形。• 终止状态是一个重条。2这些类型的状态之间的语义差异将在第4节中解释。程序有三个调用变量。S指的是将盒子连接到其订户的呼叫。用户控制盒子的功能。A和W都表示将盒子连接到远端方的呼叫;在任何时候，A是连接到订户的活动呼叫，W是等待呼叫。此功能的用户界面由两个状态信号cw指示器和开关组成。当盒子处于透明状态时，这意味着用户以正常方式连接到远端方，它可以接收呼叫变量w中的第三个呼叫。盒子发送cw指示器给它的用户以指示呼叫正在等待。 请注意，这个信号携带着等待呼叫的建立信号中的源字段作为字段;这向订户标识了新的呼叫者。每当用户希望将他的注意力从当前活动呼叫切换到等待呼叫时，他发送切换信号。这个程序在很大程度上依赖于赋值来调用变量。首先，在初始状态下，盒子在s中接收一个调用。由于DFC路由器选择呼叫等待框的方式，此呼叫可能来自或去往用户。如果调用实际上来自订户，则谓词sfrom subscriber（在文本中定义）为true如果是这样的话，它就在正确的变量中。语句ctu（s，a）通过发出一个传出呼叫，继续由传入呼叫扩展到此框的管道。另一方面，如果s来自远处，则此调用不属于s。它被重新分配给a，管道从a延续到s。最重要的分配出现在呼叫等待状态，此时用户发出交换机信号。交换a和w的值，使以前等待的呼叫现在连接到订户，而以前活动的呼叫处于保持状态。如果在呼叫等待状态下拆除，则盒子进入一种状态，其中有两个剩余的呼叫，彼此不连接。来自用户的交换机信号将导致这些呼叫被连接;它强制进行另一次重新分配，以保持活动的远端呼叫处于。第四个分配实现了一个鲜为人知的呼叫等待行为假设盒子处于呼叫等待状态，并且订户挂断（s？TDN，拆卸的缩写）。当然，这会导致盒子被拆下。W中的呼叫仍在等待。而不是把它也拆掉，盒子打电话给2CW没有明确的终止状态。扎韦和杰克森42订阅者回来了！在此之前，它会进行另一次重新分配。在赋值语句之后有一个条件分支，因为用于发出呼叫的设置信号的形成取决于现在在中的呼叫最初是该框的传入呼叫还是传出呼叫3.2协议编程很困难分布式协议必须是异步的。但由此产生的非决定性延迟、握手和竞争条件给程序增加了相当大的复杂性。在Boxtalk中，我们通过使调用的建立和拆除看起来像是原子的来解决这个问题，尽管它们不是。将rcv（c）的执行变成原子操作相对容易。如果一个setup信号在rcv（c）被使能的状态下到达盒子，实现会更新内部数据结构并发送upack作为语句执行的一部分。请注意，如果在没有启用rcv语句的情况下，设置信号到达一个框，那么该信号将自动隐式地被消除（参见第3.3节）。执行声明C？tdn意味着c中的调用已从其另一端拆除。也很容易使此语句的执行成为原子操作，因为实现只是将downack信号作为其一部分发送。语句end（c）用于启动c中调用的拆除。此语句的执行通常从发送一个拆卸信号开始。然而，结束框中的拆卸阶段并不完成，直到框在远端口接收到拆卸信号并停止发送之前首先接收到从远端口发送的每个状态信号，并且其次接收到最终的downack信号。晚到的状态信号被丢弃。端口输入队列的这种相反，它在end（c）语句执行完成后隐式地在后台发生;end（c）语句的后处理相对于程序的控制流程是异步的。如果程序员在清理完成之前重用调用变量c，那么被清理的调用将在portAllocated中，而不是在known中。终止状态（如图3所示）是程序执行的结束，但它不是表示程序语义的底层有限状态机的最终状态。 在终止状态下，portAllocated中可能仍有清除尚未完成的调用。 当portAllocated变为空时，存在从终止状态到真正的最终状态的隐式转换。用于调用的语句new（c）和ctu（c0，c）是最难实现原子化的不仅存在对确认的无限等待，而且Box程序可能有立即发送信号的需要，扎韦和杰克森43那个电话一旦发送设置信号，原子语言语句new（c）或ctu（c0，c）的执行就结束它不包括对upack的等待，即使DFC协议使得放置端口在收到此确认之前不可能发送呼叫信号。如果随后的程序语句在此调用上发送信号，则输出信号在内部排队，并在收到upack信号例如，程序可以执行语句序列ctu（c 0，c）; c！s1; c！s2;other，其中other不为非选择调用c。 虽然这是不可见的程序员，其他实际上可以在c之前执行！s1; c！s2，如果c？直到Other完成之后才发生UPACK。表观序列和实际序列是等效的，因为信号s1和s2到达呼叫c的另一端可能需要任意长的时间。因此，end（c）、new（c）和ctu（c0，c）语句的语义都需要隐式后处理，该后处理相对于程序的控制流程是异步的。这是一个温和的复杂性，我们认为这是Boxtalk的一个主要优势;如果这种复杂性没有内置到语言的语义中，那么每个盒子程序员都必须为自己编程Boxtalk的语义只需要验证和实现一次。在Boxtalk程序的语义中，在执行rcv（c）、new（c）或ctu（c0，c）状态之后，在执行end（c）或c之前，带有c中标识符的调用被认为是活动的。tdn声明。活动调用是重要的，因为它们是Box程序员唯一可以操纵的。它们是如此重要，以至于程序员必须用指向所有活动调用的调用变量来标记每个稳定状态。（如第5.2节所述，该信息是多余的所有对调用进行操作的Boxtalk语句都有基于相关调用是否处于活动状态的先决条件：• C的前提条件！状况C？status、end（c）和c？TDN是C指向活动呼叫。否则，该语句是未定义的，违反了DFC协议，或两者兼而有之。• rcv（c）、new（c）和ctu（c0，c）的前提条件是c不指向活动呼叫。否则就违反了每个活动调用必须是某个调用变量的值的不变量。• 由于相同的不变量，在一个赋值语句中，如c1，c2 = c2，-，任何不出现在右边的变量，如c1，都不能指向一个活动调用。包 含 所 有 活 动 调 用 的 标 识 符 的 setactive 是 portAllocated 和known的子集。然而，它不是这两个集合的交集处于清理阶段的调用，其调用变量尚未被重新分配不同的值，则在portAllocated和known中，并且不处于活动状态。扎韦和杰克森44IBFBFBIB设置乌帕克设置乌帕克设置乌帕克无效无效teardownteardown下背包下背包3.3需要端到端的推理假设没有功能盒，因此每个DFC内部调用都由一个接口盒发出，并由一个接口盒接收。如果目标地址无效或目标接口盒忙，路由器可以直接向放置盒报告问题。 如果收到的放置箱一个UPACK信号，它将知道呼叫已经成功地到达另一个接口盒。另一方面，在组件体系结构中，情况非常不同，如图2所示此图是一个消息序列图，显示了两个接口盒和两个功能盒之间的详细信令图二、组件体系结构中信令的分段性质图2显示了每个内部调用在管道之前完成继续进行。有必要在组件架构中以这种方式组织信令。如果每个特征框没有立即确认传入的设置信号，而是等待从目标接口框接收结果，则所有特征框将被冻结，直到流水线到达端点。他们的电话都不会被建立，没有一个盒子可以发送或接收任何信号。作为组成部分，它们的自主性和实用性将非常有限。然而，正是因为呼叫建立是分段的，所以它不提供任何端到端信息。DFC协议有三个内置的状态信号，旨在提供有关通信尝试结果的端到端信息。这三个信号是未知、无效和有效。它们涵盖了本节第一段中提到的三个结果。在图2中，目标设备不可用。第一个功能框由unavail信号触发;它将向扎韦和杰克森45--呼叫者，如转发、语音邮件或自动重试。它吸收了来自下游的无效信号和拆除信号，因为如果它将它们传播到上游，呼叫者可能会挂断电话。显然，一个成功的盒子程序员必须考虑他的程序的端到端和分段后果。换句话说，程序员必须考虑实现盒子的预期功能，以及当盒子不执行特定功能时使其透明。 分段和功能性思维往往更自然，所以Boxtalk尽可能地帮助端到端和透明的编程。这种语言的第一个也是最重要的特征是信号连接。在稳定状态下，如果两个活动调用的调用变量组合在带括号的对中，则它们是信号链接的。如果两个活动呼叫是信号链接的，则对来自任一呼叫的任何状态信号的默认处理是将其转发到另一个呼叫。例如，在CW的透明状态下，两个活动呼叫是信号链接的。如果一个盒子转发两个信号链接调用之间的所有状态信号，则该盒子是不可观察的。由信号链接建立的信号的缺省处理可以被显式转换覆盖.例如，CW盒从不转发来自用户的交换信号，因为该信号仅作为用户命令对该盒有意义三个稳定状态中的每一个都有一个由来自用户的开关信号触发的在透明状态下，它具有重要作用。在一个稳定的状态与积极的调用c和没有显式的过渡c？从呼叫C接收到拆除信号自动地并隐含地终止整个Box程序，其包括结束所有其它活动呼叫。例如，在CW程序中，没有从透明状态的显式拆卸转换-如果任何一方挂断，其接口框开始拆卸的连锁反应，应该很快删除整个框和内部调用的图形。另一方面，在呼叫等待状态中，在每个活动呼叫的拆除上存在显式转换。由于有三个活动呼叫，因此其中任何一个都是无效的。为了帮助说明呼叫抽象的其余方面，我们介绍了一个用于顺序信用卡呼叫（SCCC）功能框的程序（图3）。此功能使呼叫者能够在输入帐户信息后在r中接收到呼叫时，程序首先对能够实现与呼叫者的交互式语音响应对话新语句上的creditquery summix表示程序的文本部分提供了各种参数字段;这些字段指定调用的目标是具有“credit query”程序的服务器在信用查询状态下，通过v中的调用到达的资源是扎韦和杰克森46{无效的帐户/ v！重启不良信用v？结果good_credit /end（v）; ctu（r，e）是吗？TDNr？return（e）;新的（v）联系我们r？disconnect/ new（v）联系我们invalid_address/v！重启v？结果valid_address / end（v）; ctu（r，e）{new_address}图三. 一个顺序信用卡呼叫功能框。提示呼叫者输入账号并收集该号码的数字。当它收集了一个完整的号码并检查了数据库的状态时，资源首先向调用者宣布信用检查的结果，然后发送一个信号结果。特征框对该信号的内容进行条件分支。如果帐户是一个坏的，盒子程序现在终止。如果帐户是一个好的帐户，功能框将发出一个呼出呼叫，继续在r中进行呼叫的管道。此时，盒子变得透明。但是，如果主叫方选择通过发送特殊的断开信号而不是通过挂断电话来断开与被叫方的连接，则功能框将主叫方连接到提示并收集新电话号码的资源。如果此对话成功，该框将在同一帐户上设置新的呼出呼叫。一旦这个程序通过了信用检查，导致终止的唯一事件是从r中的调用接收到一个拆除信号。我们现在回到结果状态信号的主题。典型地，调用者的接口盒将它接收到的结果信号转换成一些已放弃：r透明：（r，e）addr_query：（r，v）注册资本（r）/credit_query：（r，v）new（v）credit_query}扎韦和杰克森47呼叫者可观察到的状态指示符。在PSTN中，例如，unavail刺激忙音，unknown刺激错误音，avail建立从网络到设备的语音通道如果没有特征，则由接口盒发出的传出呼叫将具有确切的一个结果。在存在特征的情况下，情况很快变得更加复杂。例如，假设一个无应答呼叫转移（CFNA）功能被触发并转发到一个电话，很忙。首先，呼叫者3然后CFNA功能由超时触发，结束其当前传出呼 叫 ， 并 将 另 一 个 呼 出 呼 叫 转 到 转 接 号 码 。 这 个 呼 叫 的 结 果 是unavail，当它到达呼叫者的接口框时，会发出忙音。对许多特性的考察是绝对有说服力的：一个调用接口盒可以接收任何序列的输出信号。它对调用者的行为仅由最近的一个决定这意味着结果信号是幂等的。这也意味着我们需要第四个结果信号none，表示“还没有结果”。从下面的SCCC示例中可以清楚地看出这一点如果一个特性以任何不平凡的方式操纵调用，那么特性程序员就很难正确和一致地处理结果信号。出于这个原因，我们在Boxtalk中构建了正确的结果处理考虑一个有一个呼入和一个呼出的盒子。结果处理的基本规则是，无论何时两个呼叫是信号链接的，最近发送到呼入呼叫的结果应该是呼出呼叫的最新结果。如果这两个呼叫在发出呼叫后立即成为信号链接每当传出呼叫的结果到达时，它将自动转发到传入呼叫。为了处理更复杂的情况，实现必须存储每个活动传出呼叫的最新结果（结果被初始化为none）。每当一个呼入呼叫成为新的信号链接到一个呼出呼叫，实现自动发送最新的结果来传入呼叫。例如，假设SCCC程序处于透明状态，并且e的结果是无效的。通过r连接到此框的呼叫者听到忙音，并发送断开信号，以便他可以尝试另一个号码。他希望忙音立即停止，即使在连接到资源时可能会有延迟。这种有利的行为将被实现，因为一旦r成为与v信号链接的，盒子将向r发送v的当前结果，即无。无信号将3回铃音和提示音是媒体级信令现象，而不是呼叫级信令现象。信号，因此本文中不讨论它们扎韦和杰克森48使忙音静音，稍后将跟随来自资源的avail。如果e的目标不可用，则很可能会拆除下游呼叫，此框将转换为放弃状态。请注意，此转换不会导致自动发送任何结果信号-它们是在获取信号链接时发送的，而不是在删除信号链接时发送的。这是适当的，因为呼叫者应该继续听到忙音，直到他发送断开信号或挂断。结果处理实际上比这更复杂一些，仅仅是因为许多图具有比单方向管道更复杂的形状和历史。然而，所有情况下的原理都是相同的，所以最简单的情况应该足以传达基本思想。4形式语义与验证4.1语法我们首先对语言语法做一个非常简短的概述。本概述省略了许多细节和不相关的方面，包括根据本文所述结构从语法上讲，程序是一个连通图，其节点表示控制状态。它们分为四类，并受到以下限制：• 只有一个初始状态，没有内转换。• 存在任意数量的瞬态。一个瞬态至少有一个输入转换和一个输出转换。• 有许多稳定的状态。一个稳定的状态至少有一个过渡.• 存在任意数量的终止状态。 终止状态具有至少一个入转变而没有出转变。附于该控制结构的程序由三种程序元素组成：• 一个无条件语句是一个总是被启用的语句（前提是它的前提条件被满足，这是5.2节的主题），例如new（c），ctu（c 0，c），end（c），c！身份和任务• 条件语句是一种仅在输入队列中存在特定信号时才启用的语句，例如rcv（c）和c？status.• 一个条件只是一个关于盒子状态的谓词瞬态可以用无条件程序来标记，无条件程序是无条件语句的序列。一个过渡的瞬态标记的一个条件，然后可选地由一个无条件的程序。如果条件为真，则启用转换每个稳定状态都必须用所有活动调用的变量来标记扎韦和杰克森49在那个州。初始或稳定状态的输出转换被标记为条件语句，随后可选地是无条件程序。如果条件语句被启用，则转换被启用4.2语义现在我们对语言语义学做一个非常简短的概述。它也可以用有限状态机来描述，其控制状态与语法状态非常相似。唯一的区别是终止状态和最终状态。无论语法使用一个、零个还是多个终止状态，语义都只有一个终止状态。语义也有一个最终状态，从终止状态通过隐式转换到达。请注意，稳定状态可能没有显式的输出转换，因为它的所有输出转换都是隐式的，包括在拆卸信号时转换到终止状态（第3.3节）。盒子的动作可以用两种方式划分，导致四个类别。一个动作可能是由进入一个状态触发的，也可能是一个状态的输出转换一个动作可能是显式的，基于程序中编写的内容，也可能是隐式的，是程序语义的结果如果一个过渡状态被标记为无条件程序，一个明确的动作进入那个状态。执行无条件程序。在进入稳定状态时可能有一个隐含的动作。如果在状态中有新的信号链接，结果信号将自动发送在进入终止状态时可能存在隐式动作。如果有活动呼叫，则全部结束。初始、稳定和终止状态都是响应状态，这意味着盒子正在关注它的输入队列。瞬态是没有响应的，这意味着盒子没有注意到它的输入队列。响应性的重要性将在第5.3节中进一步讨论。瞬态的所有输出转换都是显式的。在瞬态中，如果启用了至少一个输出转换，则非确定性地选择并执行启用的输出转换。响应状态具有隐式转换以及程序语法中给出的显式像显式转换一样，所有隐式转换都是由盒子的输入队列中存在的信号触发的。存在隐式过渡有两个原因• 隐式转换的存在只是为了使程序员不必显式地编写它例如，每一个没有由rcv语句触发的显式转换的响应状态都有一个隐式的输出转换，它响应图2中的目标接口框所做的设置，并返回到相同的状态。• 隐式转换是一个新的，扎韦和杰克森50CTU或者结束声明例如，由upack和downack是隐式转换。在响应状态中，如果启用至少一个出转变，则非确定性地选择并执行启用的出转变。如果没有启用输出转换，则执行暂停，直到通过接收新信号启用一个输出转换。4.3验证DFC协议已在Promela中指定，并使用Spin模型检查器进行检查[10]。假设所有的功能框都是输入使能的（见5.3节），并且遵守协议，那么就不会有死锁、丢失信号或无关信号。为了证明Boxtalk的语义是合理的，我们应该验证所有程序都满足DFC协议的安全属性，并且保持了box状态的各种不变量（其中一些在第3节中已经提到）。本节描述了执行该验证的计划第一步是处理隐式操作。如果我们引入一些伪语句，比如c？upack和c？downack，它实际上不能在Boxtalk程序中使用，那么所有隐式操作都可以显式编写。换句话说，一个Boxtalk程序可以被预处理，以产生一个带有伪语句的中间程序，而没有任何类型的隐式操作。我们要检验的正是这种中间形式的程序一 个 盒 子 的 状 态 显 然 包 括 它 的 局 部 变 量 的 值 ， 像 active 和portAllocated这样的集合，像把portAllocated中的调用映射到它们的端口的函数，等等。我们已经部分地将语句和伪语句指定为对这个状态的操作。我们还在Alloy [11]中指定了这种状态的一些正确性不变量盒子的状态可以扩展为包括每个端口的输入队列、每个端口的协议状态以及每个端口的输出队列中最近发送的信号。这个扩展有两个目的：（1）它使我们能够根据队列修改来指定语句的信令行为，因此语句和伪语句可以完全根据状态上的操作来指定。(2)它使我们能够在操作的前提条件和后置条件方面我们希望，在扩展了盒子状态并以这种方式完成了操作的规范之后，我们将能够验证不变保持和协议遵从性。每个操作的假定前提条件将从它可能发生的上下文和句法分析中推导出来（见5.2节）。我们还希望使用Alloy约束分析器来自动化一些验证。扎韦和杰克森515必要性质5.1图约束本节中讨论的两个属性都需要对Boxtalk程序进行额外的语法限制。在程序图中，两个响应状态之间的每条路径必须是无环的。例如，图4所示的图形作为Boxtalk程序的基础是不合法的，因为在两个稳定状态之间有一条路径，其中有一个循环。见图4。 非法程序图。请注意，此限制并不妨碍瞬态收敛。例如，图5所示的图形是合法的。图五. 一个合法的程序图。扎韦和杰克森525.2无运行时错误防止组件体系结构中的运行时错误尤为重要。有更多的独立程序协同运行，对它们来自哪里的控制更少。在电信领域，组件体系结构的主要动机之一是允许客户可编程性。如3.2节所述，所有对调用进行操作的Boxtalk语句都如4.3节所述，我们打算证明，如果语句的前提条件在语句执行时得到保证，则语句将成功执行，没有运行时错误。由于5.1节中的约束，连接两个响应状态的路径是有限的。每个路径对应于一个已知的显式语句序列。例如，从SCCC的信用查询状态到透明状态的路径对应于序列v？result; end（v）;ctu（r，e）.因此，有一种分析算法可以检查所有与调用相关的语句的先决条件。它只是遍历响应状态之间的每条路径，跟踪活动调用集，并在执行时检查先决条件。对于每个路径遍历，活动集被初始化为路径开始处的状态标签中的集合（假设初始状态被标记为空集）。一旦路径遍历完成，活动集必须匹配路径末尾的状态标签（除非路径在终止状态结束）。例如，遍历上面提到的路径将计算活动集如下：credit_query状态v？结果end（v）ctu（r，e）透明状态{r，v}{r，v}{ r}{r，e}很明显，路径上所有语句的前提条件都得到了满足，并且生成的活动集与透明状态的标签相匹配。这种分析不需要考虑隐式动作。每个隐式操作都可以在其发生的状态下显示为有效。改变活动调用集的唯一隐式操作是进入终止状态时的隐式操作。根据定义，它结束所有活动呼叫，并在进入没有活动呼叫的状态之前。该算法表明，稳定状态的标签是冗余的（仅扎韦和杰克森53只要它们显示活动的呼叫集-信号链接不是冗余的）。由于每个稳定状态都是从初始状态可达的，所以该算法可以用来计算它的标签。标签在Boxtalk中是必需的，因为它是一种有价值的冗余形式。5.3框启用输入如果一个盒子保证及时读取每个输入队列中的每个信号，那么它就是输入使能的。输入使能在组件体系结构中非常重要，因为它可以防止死锁并使组件对其输入做出响应。例如，即使一个盒子所有Boxtalk程序都是启用输入的，只要它们的实现在启用的转换中做出公平的非确定性选择，并且它们通过一个额外的检查（见下文）。关于输入使能的论证有两个部分：（1）程序在每个响应状态下都是输入使能的。(2)在离开响应状态时，程序总是在有限的时间间隔内返回到响应状态。响应状态是启用输入的论点很简单：由于Boxtalk的所有隐式特性，在每个响应状态中，都有一个由每个可能的输入队列中的每个可能的信号触发的输出转换。例如，尽管前面没有提到，但考虑当程序处于稳定状态时，调用c的输入队列中的状态信号s。如果c当前没有信号链接到任何其他调用，并且如果c上没有显式转换？s，则隐式转换读取s并将其丢弃。一个盒子迅速返回到响应状态的论点始于这样一个限制，即响应状态之间的路径是非循环的，因此是有限的。如果每个语句的执行时间是有界的，并且在路径上的某个地方不可能有执行块年龄，则路径的执行时间将是有界的。Boxtalk语句仅限于执行时间有限的语句。所有调用操作语句都设计为具有此属性。数据操作语句也是有界的，因为它们不包括循环。（集合理解有一些受限制的特性。）一旦已经触发了从响应状态的出转变，则可能在路径执行到达另一响应状态之前停止路径执行的唯一执行场景是执行已经到达瞬态，并且从它的出转变不具有真条件。为了防止这种可能性，有必要证明，对于Boxtalk程序中的每个瞬态，out-transitions上的条件的析取为真。因此，Boxtalk程序中唯一的循环是通过扎韦和杰克森54响应国家。我们发现这是对DFC功能框的适当约束，尽管它可能不适用于其他组件体系结构或其他应用程序域。6结论已经有一些基本的工具来促进DFC功能盒的编程[3]。即将实现的Boxtalk将提供下一代功能创建工具。我们已经证明，对协调组件进行编程是一个重大挑战。程序员必须管理异步协议。适当的协调需要分段推理和端到端推理。必须保证某些组件属性。同时，组件体系结构为我们提供了一个决定哪些组件行为是等效的基础。行为等价是一种工具，我们可以应用它来选择程序抽象和简化编程。看起来至少我们的调用抽象的某些方面是可以在DFC之外应用的.任何组件异步交互的组件体系结构，例如[5，6]，可能会有一些相同的问题，并受到一些相同的解决方案。任何组件体系结构都迫切需要一种方法来证明com的良好行为无论其出处如何。引用[1] 格雷格·邦德，埃里克·张，安德鲁·福雷斯特，迈克尔·杰克逊，哈尔·珀迪，克里斯·拉明和帕梅拉·扎夫。DFC作为ECLIPSE的基础，ECLIPSE是一个IP通信软件平台。在2000年IP电信服务研讨会的会议记录中，第19-26页。2000年9月，佐治亚州亚特兰大[2] 格雷戈里·W放大图片作者：Eric Cheung，K. 哈尔·珀迪，J·克里斯托弗·拉明，帕梅拉·扎夫。下一代电信服务的开放架构。已提交出版。[3] 格雷戈里·W 邦德、弗兰乔·伊·瓦·纳·奇、尼尔斯·克拉伦德和里克·哈德·特雷泽。 ECLIPSE功能逻辑分析。第二届IP电话研讨会论文集，第49-56页。哥伦比亚大学，纽约，纽约，2001年4月。[4] L. G. Bouma和H. Velthuijsen，编辑。电信系统中的特征交互。IOS Press，Amsterdam，1994.[5] 曼弗雷德·布洛伊。交互系统的组成细化。Journal of the ACMIVIV（6）：850-891，November 1987.[6] 曼弗雷德·布洛伊。对时间敏感的通信系统的功能规范。ACM Transactions onSoftware Engineering and MethodologyII（1）：1- 46，January 1983.扎韦和杰克森55[7] M. Calder和E. Magill，编辑，电信和软件系统中的功能交互VI。，IOSPress，Amsterdam，2000.[8] K. E. Cheng和T.Ohta，编辑，电信系统中的功能交互III。，IOS Press，Amsterdam，1995.[9] 迪尼河Boutaba和L. Logrippo，编辑。电信网络中的特征交互IV。 IOSPress，Amsterdam，1997.[10] 杰拉德·J·霍尔茨曼。设计和验证协议：教程。Computer Networks andISDN SystemsXXV：981-1017，1993.[11] 丹尼尔·杰克逊，伊恩·谢克特和伊利亚·施利亚赫特。Alcoa：Alloy约束分析仪。软件工程国际会议论文集，利默里克，爱尔兰，2000年6月。[12] 迈克尔·杰克逊和帕梅拉·扎维分布式特征组合：电信服务的虚拟体系结构。IEEE Transactions on Software EngineeringXXIV （ 10 ） ： 831-847 ， October1998.[13] 迈克尔·杰克逊和帕梅拉·扎维DFC手册AT& T Research Technical Report，2001年8月。可在http://www.research.att.com上获得/info/pamela.[14] K. Kimbler和L. G.布玛，编辑。《电信和软件系统中的功能交互作用》，IOS出版社，阿姆斯特丹，1998年。[15] 玛丽·肖和大卫·加兰软件架构。普伦蒂斯-霍尔公司，1996.[16] 帕梅拉·扎维。电信功能中的地址转换。已提交出版。[17] 帕梅拉·扎维。一个架构，三个具有挑战性的功能。第二届IP电话研讨会论文集第176-187页。哥伦比亚大学，纽约，纽约，2001年4月。[18] 帕梅拉·扎维。特征工程的一个实验。成员们的文章 IFIP编程方法工作组的成员，Springer-Verlag。[19] 帕梅拉·扎维。在Promela中正式描述