DeltaCCS: A Core Calculus for Behavioral Change

TitleDeltaCCS: A Core Calculus for Behavioral Change
Publication TypeConference Paper
Year of Publication2014
AuthorsLochau, M., S. Mennicke, H. Baller, and L. Ribbeck
Conference NameLeveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change: 6th International Symposium (ISoLA 2014)
Date Published09/2014
PublisherSpringer Berlin Heidelberg
Conference LocationCorfu, Greece

Concepts for enriching formal languages with variability capabilities aim at comprehensive specifications and efficient development of families of similar software variants as propagated, e.g., by the software product line paradigm. However, recent approaches are usually limited to purely structural variability, e.g., by adapting choice operator semantics for variant selection. Those approaches lack (1) a modular separation of common and variable parts and/or (2) a rigorous formalization of semantical impacts of structural variations. To overcome those deficiencies, we propose a delta-oriented extension to Milner's process calculus CCS, called DeltaCCS, that allows for modular reasoning about behavioral variability. In DeltaCCS, modular change directives are applied to core processes by altering term rewriting semantics in a determined way. We define variability-aware CCS congruences for a modular reasoning on the preservation of behavioral properties defined by the Modal $\mu$-Calculus after changing CCS specifications. We implemented a DeltaCCS model checker to efficiently verify the members of a family of process variants.