DeltaCCS: A core calculus for behavioral change (bibtex)

by Lochau, M, Mennicke, S, Baller, H and Ribbeck, L

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. \textcopyright Springer-Verlag Berlin Heidelberg 2014.

Reference:

DeltaCCS: A core calculus for behavioral change (Lochau, M, Mennicke, S, Baller, H and Ribbeck, L), In 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2014, volume 8802, 2014.

Bibtex Entry:

@InProceedings{Lochau2014, Title = {{DeltaCCS: A core calculus for behavioral change}}, Author = {Lochau, M and Mennicke, S and Baller, H and Ribbeck, L}, Booktitle = {6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2014}, Year = {2014}, Pages = {320--335}, Volume = {8802}, 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. {\textcopyright} Springer-Verlag Berlin Heidelberg 2014.}, Doi = {10.1007/978-3-662-45234-9_23}, ISBN = {03029743 (ISSN); 9783662452332 (ISBN)}, ISSN = {16113349}, Keywords = {Behavioral changes,Behavioral properties,Calculations,Computer hardware description languages,Formal languages,Formal methods,Formal specification,Model checking,Operational semantics,Semantics,Software Product Line,Software variants,Specifications,Structural variability,Structural variations,Variability model,Variability modeling,imotep}, Mendeley-tags = {imotep}, Url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-84910649795{\&}partnerID=40{\&}md5=173c266af05a9370f3263c6c76b089fb} }

Powered by bibtexbrowser