迈向动态更新的编排与行为契约

我们综述了在多参与者交互中关于编排和行为契约的工作。特别地，提出了行为契约理论，该理论能够在不同的服务通信假设下推理正确的服务组合（契约合规性）和服务可替换性（契约精化预序）：同步基于地址或名称的通信，具有耐心非抢占或急躁调用，或异步通信。相应地，考虑了行为契约与编排描述之间的关系，其中每个通信方的契约是通过投影等方式导出的。所考虑的关系是由最大预序诱导的，该预序保持契约合规性和全局轨迹：我们证明了当考虑具有上述所有非对称通信手段的契约精化预序时，最大性成立（允许为每一方独立发现/替换服务），而当考虑标准的对称CCS/π-演算通信时（或当通过预序直接关联编排与行为契约时，无论通信手段如何），最大性不成立。所获得的最大预序随后以一种新的测试形式（称为合规性测试）来表征，其中不仅测试必须成功，而且被测系统也必须成功（因此与控制理论相关），并与经典预序（如may/must测试、轨迹包含等）进行比较。最后，介绍了关于自适应编排和行为契约的最新工作，其中上述理论扩展到更新机制，允许在运行时通过内部（自适应）或外部干预修改编排/契约。