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

Publikationstyp
Konferenz
Autor(en)
Rodger Burmeister, Steffen Helke
Jahr
2012
Seiten
193-200
Buchtitel
Theoretical Aspects of Software Engineering (TASE), 2012 Sixth International Symposium on
Organisation
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.
Link
https://ieeexplore.ieee.org/document/6269644
DOI
10.1109/TASE.2012.15
Forschungsfelder
Software- und Architekturanalyse, Parallelverarbeitung und Multicore
Download .bib
Download .bib
Eingetragen von
Rodger Burmeister