Title | DeltaCCS: A Core Calculus for Behavioral Change |
Publication Type | Conference Paper |
Year of Publication | 2014 |
Authors | Lochau, M., S. Mennicke, H. Baller, and L. Ribbeck |
Conference Name | Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change: 6th International Symposium (ISoLA 2014) |
Date Published | 09/2014 |
Publisher | Springer Berlin Heidelberg |
Conference Location | Corfu, Greece |
Abstract | 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. |