The observer pattern applied to actor systems: A TLA/TLC-based implementation analysis

Resource type
Conference
Author(s)
Rodger Burmeister, Steffen Helke
Year
2012
Pages
193-200
Book title
Theoretical Aspects of Software Engineering (TASE), 2012 Sixth International Symposium on
Organization
IEEE
Abstract
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.
Online Sources
https://ieeexplore.ieee.org/document/6269644
DOI
10.1109/TASE.2012.15
Research focus
Software and Architecture Analysis, Parallel Processing and Multicore
Download .bib
Download .bib
Published by
Rodger Burmeister