Variability Within Modelingggg Language Definitions

Variability withinModelingg Languageg g DefinitionsM í VictoriaMaríaVi t i CengarleCl 1, HansHGGrönnigerö i 2, BernhardB h dRRumpe21Softwareand Systems Engineering,TU München, Germany2LehrstuhlInformatik 3 ((Software Engineering),gg)RWTH Aachen, Germany

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenGoalSeite 2 Develop an approach with tool support to completely, formally definemodelingd li llanguages one target: UML but not exclusively: approach should work with arbitrarymodeling languages based on objects Challenges that we address obtain a precise but variable semantics (in UML terms, supportsemantic variation points) provide a flexible tool support that can be used for variousverification scenarios support underspecified and incomplete models(in contrast to complete programs) integrate semantics of multiple viewsviews, multiple models (ofdifferent types)

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenSeite 3Constituents of aModeling Language Definitionsyntaxis transformedhasconcrete syntaxabstract syntaxminimal abstractsyntaxwhile(a! x) {a ;}relatessemantic mappingsemantic domain User interacts with concrete syntax (textual, graphical, .) Internal representation as abstract syntax (AST, metamodel) andcontext conditions Minimal abstract syntax [optional](reduced set of constructs to ease code gen. or semantics definition) Well-understood, precise semantic domain S Explicit semantic mapping of syntactic constructs of language L toelements of semantic domain, sem : L (S)

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenVariabilityySeite 4 Formally handle variability in a modeling language definition Why? Modeling languages should be open to customization in aprecise and controllable way Language developers state possible syntactic or semanticvariants Users, implementers configure (i.e. choose some of the) variants Improve definition of UMLUML, currently “implementorsimplementors may provide[.] informal feature support statements [.] for less preciselydefined dimensions such as presentation options and semanticvariationi ti points”i t ” Prerequisite Analyze and classify variability

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenPresentation VariabilityysyntaxSeite 5is transformedhasconcrete syntaxabstract syntaxminimal abstractsyntaxwhile(a! x) {a ;} Variability not present in aminimali i l abstractbsyntaxrelatessemantic mapping Presentation options (as in UML) map to the same abstract syntax alternative keywords, font size, color etc. Abbreviations (syntactic sugar) enhancehreadabilityd bilit bbutt can bbeexpressed by more “primitive”constructs of the language transform hierarchical Statechartto equivalent flat Statechartsemantic domainClass Apublic int x; int y;ABCDSource StateSource StateeventeventequivalentStatechartseventsuper statet tsub state 1sub state 2 sub state 1sub state 2

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenSyntacticyVariabilityySeite 6syntaxis transformedhasconcrete syntaxabstract syntaxminimal abstractsyntaxwhile(a! x) {a ;} Variability affecting aminimali i l abstractbsyntax(and hence interacts with semantics) Language parameters leave open which languagei e.g., usedis,d tto expressconstraints or actions Syntax constraints, extensions Optional context conditions to rule outmodelsd l syntacticallyt ti llrelatessemantic mappingsemantic domainOCLJavaJ[a 0]f(a)/{x0 f( )/{ a;}}STBAC Set of valid stereotypes general principle of extending the syntaxof a language, encode semantic variability singleton A

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenSemantic VariabilityySeite 7syntaxis transformedhasconcrete syntaxabstract syntaxminimal abstractsyntaxwhile(a! x) {a ;} Subdivided into semantic domain variability semantic mapping variabilityrelatessemantic mappingsemantic domain Semantic domain and mapping analogy mapping:pp g “configurationgoptionspof a code ggenerator” domain: “properties of underlying run-time system” System Model as our semantic domain Single semantic domain for various kinds of object-basedmodeling languages Characterizes object-based systems by declaring constituents(structure, behavior, interaction) and constraining their properties Necessarily of a certain complexity, but built in a modular way,introducing a hierarchy of theories using basic maths

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenSystemyModel – highg level overviewSeite 8 Transition system : STATE (STATE) closed world, non-deterministic, timed or untimed variants States STATE DataStore ControlStore EventStore data state: attribute values of objects control state: active threads and computationalpstate of methods event state: messages to be processed Static information given through underspecified universes, e.g. UCLASS, UOID – universe of classesand object identifiers UTYPE, UVAL – universes of typesand values UOPN – universe of operations sub – sub class ameMethodTypeSaf IntEventStoreMessageLegend:extends: A Bor Auses:BAB

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenSemantic VariabilityySeite 9 Semantic domain variability system model contains variants (optional definitions) different notions of type-safe method overriding, restriction ofinheritance to single inheritance etcetc.Variant SingleInheritance C1, C2, C3 UCLASS.C1 sub C2 Æ C1 sub C3 C2 sub C3 Ç C3 sub C2 Semantic mapping variability alternative realization choices for mapping functions mapping of stereotypesVariant MapClassStereotypesmClassStereotypes stereos cl singleton stereos #(oids cl) 1

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenVariabilityy Classification SummaryySeite 10presentation variabilityvariability not present in a minimalabstractb t t syntaxtpresentation optionsaffect concrete syntax onlyabbreviationscan be omitted without losingexpressivenesssyntactic variabilityvariability affecting a minimal abstractsyntaxstereotypessyntactic encoding of semanticvariabilitylanguage parametersuseable with independent languagessyntax constraintsconstrain the set of well-formedmodelssemantic variabilityvariability in the semanticssemantic domain variabilityvariability in the underlying targetdomainsemantic mapping variabilitydifferent choices for mapping functions

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenCapturingg & Configuringgg VariabilityySeite 11 Document variants and their interdependencies which may occurbbetweenvariantsion allll llevelslvariants, others left Configure a language to fix (some) variantsunderspecified Examples: stereotype requires semantic mapping that handles it language parameter requires semantics mapping for selectedlanguage restrict multiple inheritance syntactically by context condition orsemantically in the system model or by using a delegatemechanism in the semantic mapping (choose one!) exclusive choice between two mapping functionsfunctions, system modelvariants

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenCapturingg & Configuringgg VariabilityySeite 12 Feature Diagrams to model pfeaturealternative feature. inclusion/exclusionconstraint9 selected feature9SingleInheritance.CD SemanticsvMapAssocsexcludesSystemModel.vObject rClassesmapSuperCDirect.9mapSuperCDelegate

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenOverview Tool SupportSeite 13 Possible benefits machine-readable and checkable semantics directly suitable for various verification scenarios control and quality check artifacts Focus on textual modelingg languagesg g(although conceptually metamodeling would work, too) keeping tool-support almost as flexible as “pencil and paper” ToolsT l MontiCore: framework for the modular syntax definition of textual modelinglanguages (feat. context-free grammars, embedding, inheritance) Isabelle/HOL: theoremthprover withith hihigherh orderd llogici Textual feature diagrams and configurations

Hans GrönnigerLehrstuhl fürSoftware EngineeringOverview Tool SupportRWTH Aachen(for semantic mapping and domaindomain, syntax similar)Seite 14abstract syntaxy(Isabelle/HOL)MontiCoregrammar generates feat re diagramfeatureSystemModelvObjectvTypeTypeOfAn tiSymSubLiskovPrincipleCh arAn dStrin Princ iple,BinaryAss sociationCompositeAssociationStrictSingleIn heritan naryAssoc iationValu eObjectsDerivedAssociationQualifiedAssociationSin gleTh nStaticOpnexcludes StrictSingleInheritancerequiresBinaryAssoc iationvStaterequires StaticAttrActiveObjectssystem model(Isabelle/HOL) uses uses QueryvSTSEventsStepperschedSTSrequires StepperSOSTSrequires StepperSSTSrequires schedSTS,SOSTSsemantic mapping(Isabelle/HOL)CD rCDelegate System model and its variants formalized in Isabelle/HOL (once) MontiCore translates language grammar to Isabelle/HOL data type abstract syntax as a deep embedding Semantic mapping maps abstract syntax to predicates over systems ofthe system model Feature Diagrams captures variants of the semantic mapping anddomain

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenSeite 15Example Semantic Domain and MappingConfigurationconfiguration CDCfg {SystemModel vObject e}featurediagramSystemModel {.}featurediagramCDSemantics {.}theory etheorytheory Se.SingleInheritance.multiple systemmodel configurationsare merged into oneCheck conformityt featuretof uperCDelegateMapSuperCDelegate.Generate integratedSystem Model theorytheory SystemModelimports SystemModel baseSingleInheritance.Generate semanticmappingtheory CDSemanticsimports CDSemantics baseMapSuperCDeledate.

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenVerification ScenariosSeite 16 Various verification scenarios possible Deep embedding allows reasoning about syntax, syntactic operators semantic mapping Translator for concrete models for reasoning about properties ofthese models Case studies “IntegratedIntegrated semantics of two class diagrams is empty due tocircular inheritance relationship” “A state described by an object diagram violates an OCLinvariant in a class diagram” “The sequence of messages implied by a sequence diagrammay not occur according to a Statechart specificationspecification”

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenIssuesSeite 17 Consistency (in the presence of variability) e.g., contradicting mapping functions such that m1, m2 . sem1(m1) Å sem2(m2) inconsistencies in the system model formalization so{sm valid sm} pprove that this is not so Automation for proofs currently only manually conducted proofs investigate potential for generating helpful lemmas Performance esp. with highly recursive type definitions, performancedeteriorates languages up to the size of (almost) full Java can be handled

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenConclusionSeite 18 Classification of variability that may be found in a modelingllanguageddefinitionfi i icomplete, System model-basedmodel based language Flexible tool support for completedefinition with MontiCore, feature diagrams and Isabelle/HOL support for language variants machine-checkable accessible to verification scenarios and quality control support incompleteincomplete, multiple viewsviews, multiple models types Future Work on elaborating feature model for UML how to efficiently prove configurations consistent and enhanceprooff automationtti

Hans GrönnigerLehrstuhl fürSoftware EngineeringRWTH AachenSeite 19 Thank you for your attention.

syntactic variability variability affecting a minimal abstract syntax stereotypes syntactic encoding of semantic variability language parameters useable with independent languages syntax constraints constrain the set of well-formed models semantic variability variability in the semantics semantic domain variability variability in the underlying .