软件架构：从CCS到.Net的系统方法

理论计算机科学电子笔记130（2005）151-167www.elsevier.com/locate/entcs架构原型：从CCS到.Net努诺湾罗德里格斯岛1DepartamentodeInforma‘ticaUniversidade do MinhoBraga，Portugal卢修斯山巴博萨2DepartamentodeInforma‘ticaUniversidade do MinhoBraga，Portugal摘要在过去的十年中，软件架构成为软件工程中的一个关键问题。这包括从传统的编程转向基于独立组件的部署和组装的软件开发。整个系统结构和组件之间的交互模式的规范成为工作开发人员的主要虽然有许多形式主义来表达行为，并提供不可或缺的计算能力来推理设计，但在流行的组件平台上导出架构设计的任务在很大程度上仍然是非正式的。本文介绍了一种系统的方法，从CCS行为规范中推导出NET框架中相应的体系结构框架，以可执行CCω代码 原型设计过程完全由在HASKELL中开发的特定工具支持。关键词：软件体系结构，原型，CCS，. NET。1介绍1.1动机近年来，软件体系结构的规范[8，7]已被重新认识为软件工程中的关键设计步骤它的作用是使1电子邮件地址：nfr@di.uminho.pt2电子邮件地址：lsb@di.uminho.pt1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.009152N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151明确软件系统的底层结构，识别其组成部分以及它们之间的交互动力学。也就是说，影响他们互动的行为模式。经典进程代数（例如，另一方面，CCS[14]或CSP[10]）在过去的三十年中出现，作为理解和推理交互和并发扮演重要角色的系统的演算。毫不奇怪，这种演算体现了行为和观察等价性的精确概念，以及特定的证明技术，经常被集成到通用架构描述语言（ADL）的设计中。典型的例子是WRIGHT[1]，基于CSP，DARWIN[12]或PICCOLA[11]，它们集成了许多从π演算[16，15]借用的结构。这不是本文的目的，介绍一种新的描述语言的软件体系结构，甚至没有建议额外的功能，现有的语言。我们的动机基本上是务实的：假设一个给定的系统的行为要求提供作为一个集合的进程代数表达式，这样的要求如何被纳入一个特定的系统的设计？换句话说，这些需求如何被激活，更重要的是，它们如何指导应用程序体系结构的总体设计？我们的实施目标是.NET[9]第九章：分布式应用程序设计。另一方面，行为规范是用CCS[14]符号写的。该论文的贡献基本上是在C[9]和Cω[13]之上实现此类CCS我们不依赖于特定的ADL，而是诉诸于以流行的进程代数编写的行为规范来识别其活动组件、交互词汇表和通常分布式的执行控制。这些元素指导.NET框架中应用程序框架的（自动）生成。在第2节中描述了在C这在第5节中进一步扩展到Cω。所提出的方法的系统特性通过使其自动化的可能性进行了测试：第3节描述了一个用于从CCS规范导出C为了快速参考，下一小节提供了对CCS的（相当简洁的）介绍。N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）1511531.2CCS：概述CCS符号[14]描述了通过施加在标签上的特定同步规则进行交互的标记转换结构。这种同步原则假设存在双极性的动作（称为互补，并表示为，例如，，α和α），其同时发生被理解为同步握手，外部由不可观察的动作τ表示。顺序的、非确定性的行为是由CCS中所谓的动态组合子构建的：prefix，用α.P表示，其中α表示动作，用于动作排序，sum，P+Q表示非确定性选择。惰性行为由0表示。它们的形式语义在操作上由以下转换规则给出：α。E−α→EαJE−→EJαJF−→FαJE+F−→E E+F−→F正如上面的规则所示，动态组合子可以通过完成后消失。不同的是，静态组合子沿着转换保持，因此建立了系统的体系结构。该组包括平行组合，P|Q，并限制新的K P，其中K是一组声明为进程P内部的动作，即，无法从工艺环境它们的操作语义如下：E−α→EJF−α→FJαE−→EαF−→FτE|F −→ E| FJE|F−α→E J|FE|F−α→E|FJE−α→EJnew{β}E−α→new{β}EJ（如果α∈/{β，β}）在过程项之上，是基于过程模拟彼此行为（或其可观察子集）的能力来定义的这需要一些等式定律，这些定律形成了丰富的微积分的基础，以推理和转换行为规范。例如，这些定律的范围从断言和和平行都是阿贝尔幺半群，在第一种情况下是幂等的，到强大的展开定律，它将过程的展开等同于由转移关系计算的所有导数的和。通常，由多个并行运行并相互交互的进程组成的系统的体系结构由CCS中的并发范式描述新K（P1|P2|......这是什么？| Pn)其中K是局部的子集（即，、内部）动作（或通信端口）JJJ154N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151并且每个进程Pi具有在备选执行线程之间的非空非确定性选择的形状。这样的规范格式似乎与软件架构的信息描述相当匹配，作为计算组件的集合（由进程P1到Pn表示）以及它们之间的交互（由作用域受新操作符作用域约束的操作虽然这种抽象忽略了架构描述的其他一些基本方面（即非功能特性，如性能度量或资源分配），但它为软件工程师提供了一个在这样的上下文中，下面的部分讨论如何在C中对这样的行为执行进行原型化，以设置软件系统的整体架构结构。有趣的是，由于规范符号支持一个经过充分研究的演算，因此在设计过程的早期阶段，人们就配备了正确的工具来转换架构设计2.Net Framework中的原型化行为本节重点介绍原型设计过程，从系统行为的任意CCS规范开始，在.NET中导出其骨架架构。限定性骨架在这里是一个关键词。实际上，我们的目标并不是导出整个系统，而只是诉诸行为需求，如CCS规范所表达的那样，自动导出实现的裸结构，即，它们的构建块以及相应的交互和同步限制。因此，人们并不特别关心实际值作为方法或构造函数的参数的顺序，也不关心某些特定于单个组件的最终关键算法将如何执行。在这一层次上，我们感兴趣的是诸如过程通信的方式、它们相互传递什么样的信息、它们在某个点上的内部状态、控制流程如何执行、过程如何随时间演变以及这些演变对组成系统的其他过程的影响等问题。考虑到这一点，原型设计过程将在续集中描述。2.1行动CCS规范中的动作对应于一个方法，该方法的名称等于相应实现中的动作标签。由于这些方法通常在系统中实现输入端口，因此它们总是将void数据类型作为其返回值的域。另一方面，在一项研究中，N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151155指定输出端口的补充动作（在CCS中由上划线注释表示）对应于可以返回任何有效数据类型的值的方法。方法的可访问性限制将在后面讨论。现在，让我们把所有这些方法都看作是公开的。举个例子，考虑下面的CCS规范，一个简单的自动售货机接收硬币，执行内部计算，检索硬币，最后返回到初始状态：Mcoin.τ.coffee.M在C中，硬币端口将被实现为public void onDestroy（）{稍后，在方法主体中，将定义相应的计算来处理硬币接收。另一方面，指定输出端口的coff ee端口将被转换为public void run（）{}声明一个能够返回cof类型值的方法。当然，在这个例子中，返回某个值的选择是可选的，因为返回一个被复制对象的动作可以在被复制对象方法的定义内通过一些内部计算来实现，而不是返回所需的输出。2.2过程CCS中的进程在C中对应于具有相同标识符的类这些类封装了从进程端口规范派生的所有方法。因此，在前面的例子中，我们会得到下面的C类：public classString{public void onDestruction（）{ 个 文件夹public boolean compute（）{ 个文件夹}请注意，类M通过声明和分组进程M的两个操作来实现进程M的上下文，但它仍然没有捕获其行为。事实上，类M没有方法调用顺序，而在进程M中，只有在方法coin（）被激活后才能执行方法coffee（）。此外，在进程M中，coin（）方法的执行之后紧接着coffee（）方法的执行。例如，该规范不允许在调用coffee（）之前调用coin（），或者在插入coin（）之后调用coffee（）。156N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151解决这些问题，涉及到流程执行顺序，需要在实现端增加一些控制流程代码。这就是下一小节的主题。2.3反应原型顺序端口激活（如CCS表达式中通常指定的）需要引入用于状态控制的附加变量。这个辅助变量由state表示，简单地声明为string类型，包含当前状态，由最后执行的方法的名称捕获。在操作上，每个方法都必须检查这个变量，以检查它的值是否正好是当前端口之前的端口的标识符对于与CCS规范的初始行动相对应的港口，采用略微不同的方法。在这种情况下，相应的方法必须检查变量state是否为null或包含来自当前进程（重新）执行之前的端口集的端口标识符之一这种流控制机制的实现需要引入三个基本函数来分析规范：initialPorts（P）、precPorts（P）和finalPorts（P）。它们的目的是分别识别CCS表达式上的初始操作、pre-ceding操作和final操作。一旦这些功能-的评价，其余的实现过程属于漂亮的打印和类的可访问性控制例程。然而，仍然必须防止没有顺序端口执行同步。为了实现这一点，方法必须首先将状态变量设置为特定的临时执行值（在示例中通过这种方式，不仅可以保证没有顺序端口同时执行，而且还可以获得一种检查特定端口当前状态的方法。 请注意，任何端口在系统中，要么执行一些计算（由状态变量中的值“processing“显示将上述转换方案应用于手头的示例，得到以下C代码：public classString{private string value;public void coin（）{if（state！ null ||state.Equals（“coffee”））{state=“processing”;“code from the coincomputations”state=“coin”;N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151157}else {thrownew Exception（“进程序列冲突。“）;}}公共咖啡馆{if（state.Equals（“coin”））{state=“processing”;“code from the coffeecomputations”state=“coffee”;}else {thrownew Exception（“进程序列冲突。“）;}} }个文件夹例如2.4替代反应行为规范中的替代反应由CCS非确定性选择组合子实现。在执行层面上，这种组合器被视为一种特殊的顺序控制。这在分析阶段通过函数initialPorts（P）、precPorts（P）和finalPorts（P），按预期处理选择combinator + while对检查过程进行评价。2.5限制进程内的交互限制在CCS中由新的组合器处理。它在原型级别的实现借助于.NET平台的可访问性机制。 因此，对于作用域中的每个变量，CCS限制，相应的方法被设置为内部方法，而不是像我们的玩具示例中所使用的那样设置为公共方法通过这个额外的步骤，声明为内部的方法变得只能用于同一个聚合中的类，从而将它们与其他类的可能的通过可访问性控制，可以将.NET原型结构视为流程执行域，其中每个标识符都位于精确的同样，一个问题仍然存在：该系统的边界应该在哪里？乍一看，人们可能会认为过程本身就是定义相应类的边界的好候选者然而，这种因此，最小列表方法是优选的，其中从整个系统的单个聚合开始，然后依赖于CCS表达式中的每个新出现158N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151定义过程范围和相应的有界变量。这样的作用域是在实现时创建的，导致新的聚合的构造通过采用这种用于CCS限制原型化的方法，不仅获得了进程端口的正确隔离，而且还获得了系统内的特定进程空间域，其可以被视为CCS限制的较小（子）系统。整体架构。随着子系统的引入，典型的体系结构推理的另一个特征在原型层变得明确：在整个系统的更简单和孤立的部分上安全地2.6并行架构前面的部分已经展示了如何在C3中正确地实现顺序CCS进程，但是仍然缺少一个由多个交互进程组成的系统的全貌，正如CCSpari-partial expression所指定的那样。为了解决这最后一个问题，提出了两种技术在第一种情况下，系统的执行完全由系统分析器控制在第二种替代方案中，它更接近于CCS的执行模型，流程通过内部相互反应来及时发展，直到系统达到需要与外部世界交互的点。这两种方法都提供了对整个系统的封装和一种简单的测试方法，它们都依赖于引入一个额外的类，称为系统交互类。这个类封装了整个系统，只公开它的自由变量，并确保所有组装的进程的正确执行顺序。第一种技术依赖于一个具有单一方法的类，它能够处理所有组装的进程。这要求保持所有进程的状态，并在每个动作发生时检查所有可能的交互第二种技术以类似的方式构建系统交互类，但事实上，对于每个动作发生（和相应的执行调用），执行所有内部反应，直到系统停止通信（在外部输入或输出端口上）或面临非确定性控制选择。在这一点上，人们可能会认为，以前提出的一些解决工艺限制和正确工艺顺序反应的策略，[3]实际上，这种原型设计方法可以调整到任何面向对象的语言，或者经过一些修改，甚至可以调整到经典的命令式语言。N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151159不必要的，因为系统交互类已经解决了所有这些问题。但是，系统交互类应该被看作是与整个系统交互的一种更简单的方式，而不是交互的唯一方式。在原型设计阶段，为了测试系统的各个部分，或者一般来说，测试它的任何子架构，利用单个进程或进程的域进行交互总是可能的，甚至是可取的3原型衍生为了自动应用这种方法从CCS规范中导出C架构框架，在HASKELL中开发了一个特定的工具。翻译器是基于一个两阶段的过程。第一阶段包括CCS符号的解析器，它将进程的规范转换它的实现是通过CCSParserHASKELL模块实现的，该模块利用了PARSEC库。因此，在解析阶段之后，所有CCS规范都以以下数据类型编码数据进程a =端口a（进程a）| CompPorta（工艺a）| 总和（工艺a）（工艺a）| 浓度（工艺a）（工艺a）| 新[a]（工艺a）|R呼叫| PCall（程序定义a）| ProcessEnd派生显示data ProcDef a= PDef（String， Process a）deriving显示类型Process aPDef类型构造函数接收一个进程标识符和进程定义本身的对。前者用于定义当前正在实现的进程的类，以及进程之间的交叉引用调用，由类型构造函数PCall或互补端口调用指定。数据类型Process a捕获CCS过程定义，如第1节所示，有一个微小的区别：递归调用（RCall）与非递归调用（PCall）显式区分。当然，后者要求，提供被调用进程的标识符和定义，以便在实现级别正确定义类间调用转换器的第二阶段执行C实现的计算，数据类型为ProcDef a。第二阶段由CCS2DotNet模块实现，该模块包括buildSystem函数，负责生成相应的C代码。160N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151函数buildSystem接收数据类型ProcDef a的实例，捕获CCS系统定义，并生成一系列文件，每个文件包含CCS规范中每个进程的CbuildSystem函数依赖于几个辅助函数，但其中三个实际上构成了整个自动翻译器所依赖的构建块这些功能分析CCS规范，并已在上文中作为自动实施的中心功能提到是 的 。 它 们 分 别 是 ： getFinalPorts ， 计 算 给 定 进 程 的 所 有 最 终 端口 ;getInitialPorts ， 计 算 进 程 执 行 时 所 有 可 用 的 初 始 端 口 ; 以 及 最 终portPreds，查找给定系统中给定端口的所有可能的先前端口。4例作为一个小的案例研究，考虑一个控制系统的规范，该系统管理公路和铁路之间的交叉口。注意这个例子，尽管它的尺寸很小，但它有许多特性，这些特性是这种原型方法可能有用的系统类型的典范。 首先它是一个简单而有效的系统，与体现安全关键要求的真实世界情况有关。避免死锁和安全控制流当然是需要形式化证明的性质。这可以在CCS演算中完成。一旦证明，我们的原型方法允许软件架构师得出最终实现的架构框架，因此，通过构造是正确的我们从下面的CCS规范开始，由于C。斯特灵[19]：公路有轨电车. up. ccross. dw.公路铁路有轨电车. green. tcross.red. Rail信号灯绿色.红色.信号灯+上升.dw.信号灯Cnew{green，red，up，dw}（Road|Rail|Signal）具体说明是不言自明的：基本上请注意，过程Signal确保了对控制铁路的（物理）信号量和控制公路交通的闸门的控制访问的互斥。整个系统由进程C指定，以并发范式表示，公开了整个系统使用原型生成器自动将进程C派生为N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151161NET中的骨架架构，必须执行前一节中描述的两阶段过程。为了说明的目的，我们将在这里详细考虑Signal进程，并对整个系统进行一点抽象，尽管在实现中会出现对与Signal交互的其他进程的一些调用。类似的程序适用于其他过程。在第一步中，从模块CCSParser调用函数parseCCS，对原始规范进行调用：信号=/绿色红色信号+/up.dw.信号这将相应的进程作为数据类型ProcDef a的值返回：信号=和（CompPort“绿色”（Port“红色”RCall））（CompPort“向上”（Port“dw”RCall））psignal =PDef（“Signal”，signal）一旦CCS系统被定义为ProcDef数据类型的值，只需将函数buildSystem应用于该值。功能buildSystem：： ProcDef String -> IO（）负责创建包含C类的所有文件，这些文件实现了原始过程。函数buidSystem依赖于许多其他函数，其中许多函数详尽地处理字符串和字符串操作。 为了改进这类操作，引入了一个新的类型ShowS =String->String。采用ShowS值而不是直接使用String的优点是，使用ShowS的函数组合在处理许多字符串连接的函数中保持了线性复杂性。然后，必须使用初始操作字符串（在本例中为空字符串）来刺激进程规范的最终实现，并将结果写入.cs文件或传递给其他函数。 的结果应用函数buildSystem是实现每个CCS规范中定义的过程例如，Signal.cs内容如下：使用系统;命名空间CCS {public class Functional{静态字符串状态;publicstatic void onDestination（bool b）{if（state== null）||state.Equals（“red”）||state.Equals（“dw”））{162N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151如果（！b）{Rail.green（true）; }state=“processing”;//（计算细节待提供）state=“green”;}else {thrownew Exception（“进程序列冲突。“）;}}public static void real（bool b）{if（state.Equals（“green”））{如果（！b）{Signal.red（true）; }state=“processing”;//（计算细节待提供）state=“red”;}else {thrownew Exception（“进程序列冲突。“）;}}publicstatic void onDestination（bool b）{if（state== null）||state.Equals（“red”）||state.Equals（“dw”））{如果（！b）{ Road.up（true）; }state=“processing”;//（计算细节待提供）state=“up”;}else {thrownew Exception（“进程序列冲突。“）;}}publicstatic void dw（bool b）{if（state.Equals（“up”））{如果（！b）{ Signal.dw（true）; }state=“processing”;//（需要提供计算细节）state=“dw”;}else {thrownew Exception（“进程序列冲突。“）;}}}}Signal.cs请注意，每个方法都接收一个布尔值。这与处理对互补操作的调用时的交叉引用调用有关。它的目标是防止系统在调用补充动作时进入无限循环这是通过在每个用户中强制false作为参数来实现的调用一个方法只有内部调用使用值true来调用其他com-补充行动。该协议保证每个方法都可以检查它是否被内部调用调用，因此不需要从用户调用中再次调用调用他的方法，这些用户调用需要检查是否有补充动作要调用。还请注意，每个实现进程端口的方法中的特定计算的定义仅由N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151163//（计算细节待提供）注释，使派生代码的骨架特征显式化。然而，在任何情况下，CCS表达式中指定的底层架构都已经以一种既可执行又能保证所有相关安全关键属性的方式转换为.NET5Cω中的原型Cω[13]是C语言在两个不同层次上的扩展：一方面是对XML和表操作的数据类型支持，另一方面是基于连接演算的新异步并发抽象[6]该语言为生活带来了一个并发模型，该模型足够丰富，可以应用于在单个机器上运行的多线程应用程序以及在（广域）网络上交互的异步、基于事件的组件的编排Cω对并发编程的主要贡献是引入了chord。在普通方法中，每个方法声明对应一个包含其实现代码的主体，与此相反，在chord中，方法实现可以与一组方法相关联。对应于chord的代码只有在chord头部的所有方法都被调用时才执行。这种结构与C中已经存在的异步方法的概念相结合，非常强大。注意，顺便说一下，和弦在其定义中最多可以有一个同步方法本节报告使用Cω作为原型行为规范的目标语言。经验表明，翻译变得更接近相应的CCS规范，而且更小（就编写的代码下文概述了这一方法的一些方面;读者[18]详细介绍。5.1从CCS到Cω在Cω中对CCS规范进行原型化的过程类似于相应的C语言翻译。主要分歧如下。5.1.1行动端口可以像以前一样通过方法来实现，也可以通过chord来实现，以反映依赖其他端口的情况，或者在流程执行中保持严格的顺序控制。和弦和方法的使用之间的区别，以及何时使用一个或另一个将在下面清楚地说明164N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151输出端口与需要同时执行的相应互补端口因此，它们必须由一个信号量来保护，以确保过程的顺序演进。这个信号量由异步方法实现，然后该方法被绑定到端口，如下面从进程P12实现的端口分叉1中所示，该进程P12取自下面提到的哲学家用餐问题public int findDuplicate（）;public void c_fork1（object obj）allow_c_fork1（）{ Console.WriteLine（“Phil_12 releases fork 1”）;if（objis Fork1）{&public void run（）;}return（）;}一 端口实施5.1.2反应反应的实现方式已经在上一节中部分揭示。如上所述，输出端口与规范中的相应互补端口等待被它们调用。另一方面，输入端口总是由其前任调用，因此不需要绑定到信号量以确保其正确的顺序执行。然而，需要同时执行的具有对应互补端口的输入端口也被实现为和弦以强制动作发生的同步性。这样，在这种情况下的端口必须在保持其对应输出端口的进程中执行对异步方法请求obsPort（）此调用的作用类似于请求激活，等待状态5.1.3替代反应替代反应通过将其初始端口定义为绑定到信号量（alternative（））的和弦来实现。这是一个私有的异步方法，只要备选反应的选择也可用，它就可用请注意，C方法中没有处理选择的非决定论。然而，对于Cω，它可以通过在替代反应之前的动作中执行随机选择来原型化。4在这里被理解为原子性，在这个意义上，两个动作都以原子的方式发生，也就是说，没有被其他事件交织。N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）1511655.1.4并行架构每个进程原型都配备了一个异步start（）方法，该方法唤醒进程并开始执行。CCS规范中的并行组合通过调用在并行上下文中组合的每个进程的start（）5.2餐饮哲学家的例子为了说明CCS行为规范如何在Cω中原型化，开发了用餐哲学家问题的解决方案[4]。由于篇幅所限，本文无法讨论该示例，[18]第五章有趣的是，从CCS规范开始，将本文讨论的方法获得的原型与Cω文档[13]中提供的相同问题的直接实现进行比较。在后者中，系统中每个实体的界限不明确，它们相互作用的手段也不明确，资源共享也不明确。另一方面，[18]中的Cω原型非常紧密地遵循原始CCS规范，这需要对解决方案进行简洁的描述，对介入实体进行明确的定义，并对每个实体的行为进行精确的概念。此外，所有的交互词汇表都建立在函数main中，它也处理进程实例的激活因此，生成的Cω代码更容易理解和分析。6结论和今后的工作本文是[17]的扩展版本，提出了一种简单但功能强大的方法，用于自动推导CCS中编写的行为规范的C和Cω原型。 由此产生的代码可以在许多不同的上下文中使用。例如，在互联网中大量存在的无状态环境下开发的应用程序，与Web服务特别相关以最后一种范式为目标，可以很容易地在（内部/内部）网络中分布进程，并使用SOAP来管理所有外部方法调用。其动机正是使用形式化方法时通常会被调用的动机：首先诉诸形式化符号，以实现需求的精确表达和计算能力，以讨论正确性和细化。然后，在更接近工作程序员关注点的合适的实现框架中导出可执行原型。5 相应的Cω代码可从www.example.com获得wiki.di.uminho.pt/wiki/bin/view/Nuno。166N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151我们相信，工作的程序员越来越多地成为工作的软件架构师，他们的工作本质上是寻找合适的软件组件，并插入它们，以保证某些期望的性能。如果说CCS看起来是一种可靠的、相对知名的计算形式主义，那么.NET几乎正在成为实现基于组件的应用程序的事实上然而，该方法在很大程度上独立于CCS的交互规程：例如，也可以容易地结合在一些流行的ADL或广播通信中使用的类似CSP的在任何情况下，重点从单机编程转移到架构设计，在这种意义上，我们相信，在本文中勾勒的approach可能会发现在实践中有用。应该提到的是，这个想法已经被用于遗留系统的架构重建项目的背景下，以及在一个软件架构的本科课程教计算机科学学位的三年级学生在米尼奥大学。目前的工作包括• 测试类的生成和基于Web的原型测试接口的派生。• 从π演算中的行为规范开始，将原型设计方法扩展到移动应用程序[15]。• 将这种方法集成到软件体系结构的正式规范的方法这基本上需要建设一个图书馆典型软件连接器的规范，以及相应的.NET骨架，能够在建筑设计中重复使用。回想一下，软件连接器[7，5，2]是一种抽象，旨在表示组件之间的交互模式，后者被视为主要的计算元素或信息存储库。连接器的目的是调解组件之间的通信和协调活动，充当它们之间的粘合代码。示例范围从简单的通道或管道，到事件广播器，同步屏障或甚至更复杂的结构编码客户端-服务器协议或数据库和应用程序之间的集线器。所有这些都可以用进程代数表示法来指定（例如，，[1，12]），因此，翻译为。最后，应该提到的是，C本身也在朝着在语言级别上集成原语分发和并发控制原语的方向发展[3]。如第5节所述，这为架构原型提供了更丰富致谢。 这项研究是在以下背景下进行的PURE项目（项目理解和重新设计），N.F. 罗德里格斯Barbosa/Electron.注意Theor。Comput. Sci. 130（2005）151167根据POSI/ICHS/44304/2002号合同提供。引用[1] R. Allen和D.加兰架构连接的正式基础。ACM TOSEM，6（3）：213[2] M. Barbosa和L.巴博萨软件连接器。在K。Araki和Z. Liu，editors，Proc. 第一次国际计算理论讨论会（ICTAC'04），中国贵阳，第53-68页。Springer Lect. Notes Comp. Sci.（3407），2004年。[3] N.本顿湖Cardelli和C. Fournet。C语言的现代并发抽象。在Proc. ECOOP 2002中。施普林格大学注释对比Sci. （2374），2002年。[4] E. W.迪杰斯特拉协作的顺序进程。Technical report，Technische Universiteit Eindhoven，The Netherlands （ reprinted inProgramming Languages ， F.Eduyys （ ed. ） ， AcademicPress，New York，1968，43-112），1965年9月。[5] J. Fiadeiro和A.洛佩斯架构连接器的语义。在TAPSOFT'97的Proc.施普林格大学注释对比Sci.（1214），1997年。[6] C. 去你的，G。 去那边，J。-J. 我很好，我。 Marannget，andD. 好的。计算多个数据类型。在Proc. CONCURSpringer Lect. Notes Comp. Sci.（1119），1996年。[7] D. 加 兰 软 件 体 系 结 构 的 形 式 化 建 模 与 分 析 ： 组 件 、 连 接 器 和 事 件 。 In M.Bernardo 和P.Inverardi，编辑，第三届计算机、通信和软件系统设计的形式化方法国际暑期学校：软件体系结构（SFM 2003）。Springer Lect. Notes Comp. Sci，《自然科学》，（2804），意大利贝尔蒂诺罗，2003年9月。[8] D. Garlan和M. 肖软件体系结构导论。在V. Ambriola和G. Tortora，编辑，软件工程和知识工程的进展（第一卷）。世界科学出版公司，一九九三年[9] E.刚纳森一个程序员2000年出版[10] C. A. R. 霍尔通信顺序进程。计算机科学系列普伦蒂斯-霍尔国际，1985年。[11] M. 兰普一种基于π演算的软件组合方法。博士论文，伯尔尼大学，1999年1月。[12] J. Magee，N.Dulay，S.Eisenbach和J.克莱默分布式软件架构。1995年第五届欧洲软件工程会议[13] Microsoft Research. CωDocumentation，2004.[14] R.米尔纳通信和并发。计算机科学系列Prentice-Hall International，1989年。[15] R. 米尔纳通信和移动过程：π演算。剑桥大学出版社，1999年。[16] R. Milner，J. Parrow，and D. 沃克移动过程的演算（第一部分和第二部分）。信息与计算，100（1）：1[17] N. 罗德里格斯和L.S. 巴博萨.Net框架中的原型行为规范以. Mota和A. 第七届巴西形式方法研讨会（SBMF《统一外交政策》，2004年11月。[18] N.罗德里格斯和L. S.巴博萨用cω开发并发系统原型。技术报告，葡萄牙米尼奥大学，2005年2月。[19] C.斯特灵流程的模态与时态逻辑。Springer Lect. Notes Comp. Sci. (715)第149-237页， 19 9 5年 。