The Observer Pattern Applied to Actor Systems: A TLA/TLC-based Implementation Analysis
The Observer Pattern Applied to Actor Systems: A TLA/TLC-based Implementation Analysis
复制标题
DOI：
10.1109/tase.2012.15
复制
发表时间：
2012-07
期刊：
影响因子：
--
通讯作者：
Rodger Burmeister;Steffen Helke
中科院分区：
文献类型：
--
作者：
Rodger Burmeister;Steffen Helke
随着参与者模型在编程语言中的影响越来越大，对反复出现的实施问题的批准解决方案的需求也不断增加。将已建立的设计模式解决方案从顺序上下文转移到并发上下文需要严格澄清意图要求和并发问题。现有方法要么不严格验证并发模式实现，要么不解决参与者模型。为了解决这些不足，我们 (1) 使用 LTL 表达式和抽象轮廓指定有意的需求，以及 (2) 使用模型检查技术将这些需求转移并验证为具体的、基于参与者的 TLA 描述。我们的方法的适用性在众所周知的观察者模式的并发版本中得到了证明。我们的工作使软件工程师能够为顺序和并发设计模式实现建立正式的需求目录，并轻松地对其进行严格验证。
With the increasing impact of the actor-model in programming languages, there is also an increased demand for approved solutions for recurring implementation problems. Transferring established design pattern solutions from sequential contexts to concurrent ones requires a rigorous clarification of intentional requirements and concurrency issues. Existing approaches either do not verify concurrent pattern implementations rigorously or do not address the actor model. To solve these insufficiencies we (1) specify intentional requirements using LTL-expressions and an abstract outline, and (2) transfer and verify these for a concrete, actor-based TLA description using model checking techniques. The applicability of our approach is demonstrated for a concurrent version of the well known Observer Pattern. Our work enables software engineers to build up formal requirement catalogs for sequential and concurrent design pattern implementations and to rigorously verify them at a low effort.