Towards Inconsistency Tolerance by Quantification of Semantic Inconsistencies István Dávid Eugene Syriani University of Antwerp - Flanders’ Make, Belgium University of Montreal, Canada istvan.david@uantwerpen.be syriani@iro.umontreal.ca Clark Verbrugge Didier Buchs Dominique Blouin HPI, University of Potsdam, Germany McGill University, Canada University of Geneva, Switzerland Telecom ParisTech School, France clump@cs.mcgill.ca didier.buchs@unige.ch dominique.blouin@telecom-paristech.fr Antonio Cicchetti Ken Vanherpen Mälardalen University, Sweden University of Antwerp - Flanders’ Make, Belgium antonio.cicchetti@mdh.se ken.vanherpen@uantwerpen.be ABSTRACT more statements about the system are made that are not jointly sat- Due to the increase of their complexity, currently engineered sys- isfiable. tems cannot be developed by one individual, but are a product of a While dealing with inconsistencies has been a well-researched collaboration between multiple stakeholders who develop the sys- topic, most approaches focus on maintaining consistency in terms tem from different domain-specific views. Inconsistencies between of syntactic relationships between models [23, 25, 26, 40]. These views, however, hinder collaboration and therefore, must be man- approaches, however, fall short of properly addressing the problem aged. Since the encountered inconsistencies may potentially dis- of semantic inconsistencies, which are typical in collaborative set- appear as the natural consequence of a design workflow, tolerating tings where disparate formalisms of various domains are involved, them to a given extent may be desirable and can lead to a more effi- e.g. when engineering mechanical and control parts of a CPS. cient collaboration. A key to reason about tolerance is the quantifi- Finkelstein [21] suggests that instead of simply removing incon- cation of the impact of single inconsistencies on the overall system sistencies from the system from time to time, one should manage design. consistency. This entails characterization and detection of incon- In this paper we present a quantification model for semantic in- sistencies before resolving them, and the subsequent analysis. In- consistencies in discrete and continuous systems. We investigate consistencies are, however, stateful entities that might occur, evolve characteristic behavioral patterns of inconsistencies based on this and later potentially disappear as the natural consequence of a de- model and identify the links with various forms of tolerance. Fi- sign workflow. This gives room for temporarily tolerating them [4], nally, we discuss the directions of further expanding the approach i.e. allowing inconsistencies to exist for a period of time, which required for a comprehensive inconsistency tolerance technique. promises lower resolution costs by (i) postponing resolution to a more appropriate phase of the design process; or, in some cases, even (ii) completely avoiding resolution when specific inconsisten- Keywords cies get resolved on their own. inconsistency management, inconsistency tolerance, temporal tol- Deciding whether or not to intervene in an inconsistent situation erance, multi-view modeling, collaborative modeling requires information about (i) how severe the inconsistency of the whole model space is; and (ii) what are the chances that the incon- sistency gets resolved without intervention. In this paper, we focus 1. INTRODUCTION on the first question and present a quantitative approach for assess- The complexity of current engineered systems has increased dras- ing the severity of semantic inconsistencies. For that, we formalize tically over the last decades. Pertinent examples are today’s mecha- the notion of (in)consistency in multi-view modeling by defining tronic and cyber-physical systems (CPS). Due to their complexity, a relation between a property of the whole system, the satisfaction these systems are no longer engineered by a single individual, but of the property by individual views, and the consistency between rather by the collaboration of experts. Such collaborative endeavors views. We identify characteristic behavioral patterns of properties involve stakeholders from different domains, who bring their point in terms of their consistency and use these patterns for guiding the of view on the system to be built, resulting in typical settings of tolerance. The results of this paper serve as formal foundations multi-tool and multi-view modeling (MVM) [37, 47]. Collabora- to implement a consistency management framework for collabora- tive environments are further characterized by multi-formalism and tive modeling scenarios with multi-paradigm and multi-abstraction multi-abstraction, meaning, different formalisms and languages are characteristics. used to support each team of stakeholders. In Section 2, we give an overview on multi-view modeling along Models of different views must be kept consistent in order to with an illustrative example used throughout the paper. In Sec- develop a correct system. However, as stakeholders develop the tion 3, we provide a quantitative model for assessing the severity respective domain-specific parts of the system independently from of semantic inconsistencies. In Section 4, we show how the pre- each other, models from these domains can become inconsistent. viously defined quantitative model can be extended to support tol- Following the definition of Herzig et al. [36], this means two or erance of parameter inconsistencies and temporal tolerance of in- To reason about characteristics of the semantic domain of mod- consistencies. We also discuss the directions of further expanding els (such as overlaps and linked properties), an explicit representa- the approach required for a comprehensive inconsistency tolerance tion of the semantic domain has to be provided. In this paper, we technique. Finally, we discuss the related work in Section 5 and consider models M expressed with an operational semantics JM K, conclude our paper with Section 6. consisting of traces on given states. 2. OVERVIEW ON MULTI-VIEW MODEL- 2.2 Motivating Example ING In this section, we give an overview on the context of our work 2.2.1 Collaboration models and provide a motivating example to illustrate the contributions of Our example concerns the development of complex and heteroge- the paper. nous systems such as CPS involving the collaboration of several development teams. This collaboration can be supported by cloud- 2.1 Typical Scenarios in MVM based model-based development environments such as the one pre- sented in [13]. Such environments allow the definition of view- points specifying how different views of the system under develop- ment can be constructed to be used by the various teams to interact with the models of the system. These environments can typically support two different working modes. For the simultaneous mode, any update performed on a view is immediately sent to the server for being applied to the model and changes are reflected on all other depending views. This is the way well known collaborative tools work, such as Google Docs or Overleaf, which were used to write this paper collaboratively. However this simultaneous mode may not meet the needs of all Figure 1: Scenarios in multi-view modeling. development organizations. For example, large and complex sys- tems are often decomposed into subsystems developed by different entities (e.g., manufacturers, suppliers, subcontractors, etc.). Fur- Corley et al. [13] identify four typical collaborative modeling sce- thermore, due to intellectual property protection concerns, the mod- narios shown in Figure 1. In Multi-User Single-View settings (Sce- els may never be allowed to cross the boundaries of an enterprise lo- nario 1), users work on the same view of the model and observe the cal network. Then, a system integrator needs to plan ahead of time a exact same data in the same concrete syntax. The other three sce- series of virtual integration steps where the models developed by all narios are characteristically different as they feature multiple views external entities are integrated and analyzed for various properties. or multiple models, which are the primary cause of emerging in- Consistency of the system as a whole then needs to be checked as consistencies. In Multi-View Single-Model settings (Scenario 2), the models have evolved independently for a given period of time. users work on different views of the model. The two views may According to the analysis results, decisions and updates will then use different concrete syntax. The views are projections of the be made to restore consistency. We call this mode delayed commit. same single underlying model (SUM) and therefore conform to the The frequency of such virtual integration steps may vary but has same modeling language. Changes in the abstract syntax of one to be carefully considered, e.g., to avoid the large costs potentially view have to be reflected in the other view in order to retain consis- induced by the rework of highly inconsistent models. In this mode, tency. The Multi-View Multi-Model scenario (Scenario 3) does not providing a measure that quantitatively determines how inconsis- assume a SUM, but multiple separated underlying models, which tent the models are is highly relevant. are connected via their semantic domains. Manipulating the mod- els throught the respective views causes mismatches in the models themselves and thus, inconsistencies may arise. Finally, the Single- 2.2.2 The Automated Guided Vehicle View Multi-Model scenario (Scenario 4) is a special form of the Our running motivational example is the collaborative model- Multi-View Multi-Model scenario, in which one view corresponds based development of an Automated Guided Vehicle (AGV) (Fig- to multiple underlying models. In practice, collaborative modeling ure 2). According to the stakeholder requirements specification, the settings typically feature combinations of these scenarios. AGV needs to be able to transport a number of objects by follow- The views can belong to different domains, i.e. they may rep- ing a given trajectory with a given maximal tracking error. Further- resent various aspects of the SUM in different formalisms and on more, it needs to have a given autonomy as defined by the number different levels of abstraction. A typical example is the mechanical of trajectories that can be followed before needing to recharge the design of a complex system where multi-body models and more AGV’s empowering component. Finally, the mass of the AGV must detailed finite element models are used to reason about different not exceed a given value because, for example, it will be too heavy aspects of the same virtual product. for the setting in which it is planned to operate. Inconsistencies arise due to the shared elements between views: To meet these requirements, an initial design is provided con- as one view changes an overlapping element, the change has to be sisting of a custom mechanical frame (Figure 2), an off-the-shelf propagated to the other views that share the same element, other- electrical battery, an off-the-shelf electrical motor, a drive train and wise an inconsistency will occur [22, 27]. These related elements a drive train control system. A set of viewpoints for this design is are not necessarily of syntactic nature, but they may exist in the then defined in the collaborative environment to be used for design semantic domain of the SUM as the ontological properties of the activities such as requirements specification, electric motor selec- system, e.g., safety, energy-efficiency, autonomy, etc. The confor- tion, battery selection, mechanical frame design, drive train design mance of the system to such properties can be evaluated by simu- and drive train controller design. These are listed in the header row lations or model checking. of Table 1. Requirements Mechanical Battery (VB ) Motor (VM ) Drive Train Drive Train Con- Integrated Ve- (VR ) Frame (VM F ) (VDT ) trol (VDT C ) hicle (VIV ) Battery = Battery Sup- ≥ Battery Size Support port Size Size Electrical ≤ Battery Cur- ≥ Minimum Current rent Capacity Current Capac- Capacity ity Required by Motor Power ≤ Motor Power ≥ Maximum Mo- tor Power Required by Drive Train Control System (e.g. obtained from simulation) Mass ≤ Maximum Ve- > Frame Mass > Battery Mass > Motor Mass > Drive Train ≤ Maximum = Vehicle Mass hicle Mass (ob- Mass Vehicle Mass Sup- (computed from tained from a Re- ported by Drive the sum of its quirement) Train Control Sys- constituents) tem (e.g. obtained from simulation) Table 1: Example consistency properties and statements about their values for each relevant viewpoint. erty P of the system under design, it is possible to automaticaly derive for each pair of viewpoints providing a statement about P a compound statement about the consistency of both views with respect to P . This compound statement will involve all proper- ties involved in the composed statements. For example, for P = BatterySupportSize, we obtain a consistency statement about the pair of properties BatterySupportSize and BatterySize. In Section 3, we further show how such statement can be adapted to provide a quantification of inconsistency. It should be noted that such considerations are independent from Figure 2: Overview of the Automated Guided Vehicle example. the source of inconsistency. For example, it can originate from the actual values of the underlying models used by the views, but also simply from the fact that the views are outdated due to network 2.3 System Properties and Consistency State- latency or delayed commit between the views in the cloud-based ments development environment. In order to explore different types of Herzig et al [36] define inconsistency as two or more statements inconsistency tolerance patterns as proposed in Section 4, we will that are not jointly satisfiable. In our approach, we provide such therefore consider that the two different modes (simultaneous and set of statements per system property and concerned viewpoint as delayed commit) for the cloud-based multi-view modeling environ- defined in the cells of Table 1 for the AGV example. Overall consis- ment are used for two different development processes. Example tency then consists in ensuring consistency for each given property use cases for this are provided in Section 4. of interest of the system. For a given property, consistency can be checked for each pair of viewpoints providing a statement about the 2.4 Other Applicable Cases property. From the two statements of the viewpoints, a compound While our motivating example concerns collaborative develop- statement can be derived about the consistency of both viewpoints. ment, we emphasize here that what we provide is applicable to For example, consider property P = BatterySupportSize for many other cases, thus making this proposal even more relevant. the AGV (first row of Table 1). Let us assume that there is a sin- One of them is that of runtime models and views such as those gle underlying model for the mechanical frame viewpoint and a employed in computer games implying a variety of consistency separate model for the battery viewpoint. The battery support size concerns. These are most apparent in network-based, multiplayer provided by the mechanical frame view is then simply the value games, which are both realtime environments and distributed sys- of the corresponding property in the underlying mechanical design tems, and as such bring a number of consistency concerns due to model. On the battery view however, a less precise information network latency, lossy communication protocols, and bandwidth is provided as all that can be stated for a consistent design is that limitations. Even single player games induce consistency issues, it should be greater or equal to the size of the battery. Therefore, with modern designs organized through a separation of domains only a range of values can be inferred from the battery viewpoint. in order to provide good, domain-specific performance and be- Composing these two statements, we derive the compoud statement haviour, a distinction quite visually evident in, for example, the way BatterySupportSize ≥ BatterySize, which can be evaluated collision domains are simplified abstractions of the representation at design time from the involved views VM F and VB to evaluate domain [20]. Games make a further interesting and motivational consistency. In other words, a value from the battery view outside subject due to the way consistency is tolerated - the perception- the range provided by the mechanical frame view will indicate an oriented, entertainment focus of game software means subtle in- inconsistent system. consistency is not necessarily a problem, and weaker or heuristic Generalizing this example, we can say that for a given prop- consistency guarantees are often viewed as an acceptable trade-off for increased performance or broader scope in implementation. 3.2 Measuring Distances Inconsistency management requires providing a meaningful con- 3. A QUANTITATIVE MODEL FOR ASSESS- sistency measure given the two properties and the states for evaluat- ING INCONSISTENCIES ing them. Such measure should take into account the amount of de- velopment work required to fix the inconsistency. This depends on Based on our running example, we can now provide a model several factors such as which activities must be performed to fix the for quantifying inconsistency. This can be achieved as explained design, which in turn depends on which part(s) of the design will previously for a given system property such as those listed in Table be changed to resolve the inconsistency (e.g. for our example bat- 1. We first consider consistency for a given system property P tery selection or battery support from mechanical design or both). and two given views V1 and V2 each providing a statement about One way to evaluate this is to take into account the cost of the in- P . The consistency statement composed from the statements of V1 volved development activities that will need to be performed. This and V2 about P then provides a set of two properties that must be set of activities can be determined by the graph of dependencies evaluated to evaluate the consistency statement. We then propose of the involved properties and their dependency to other properties. a metric combining these two properties to quantify the degree of However, this complex task is left for future work. For now, we inconsistency. Such measure can later be used for assessing the only provide illustrative simplified examples showing how simple importance of the inconsistency and support its management. measures can be derived for the different properties and viewpoints 3.1 Formal Definitions of Table 1. For our AGV example, the aforementioned state trace is defined The definition of consistency is based on a distance function that by the successive model states corresponding to the versions of the takes the two views and provides a measure value. In this simple system design evolving through the activities performed along a setting we need a simple domain for measures that can be used in a development time axis. compositional and associative way. Definition 1. (Measure) A given set of values M with operations 3.2.1 Battery Support Size 0 :→ M, + : M × M → M (0 neutral, + associative and commu- For the battery support size property, let us assume that the sec- tative) and an order relation ≤ on M is called a measure. tions of the battery and its support are of circular shape and can therefore be characterized by a single numerical value of the sec- Definition 2. (State distance) Given two state domains Σ1 and tion diameter. We compose the statements of viewpoints VM F and Σ2 , a distance is a function δ : Σ1 × Σ2 7→ M. VB of Table 1 to obtain a Boolean consistency statement about the From the state distance we can define by extension distances on pair of properties BatterySupportSize and BatterySize as: finite prefix of traces. By trace, we mean a sequence of perfor- ρBatterySize ≤ ρBatterySupportSize mance values [49] a semantic property exhibits as the underlying model changes. This distance is a natural extension that can ex- where ρBatterySupportSize and ρBatterySize are the property val- press the observation on a trace with a finite window starting from ues obtained from VM F and VB respectively. In such case, a simple the beginning of the trace. The size of the window λ is a parameter measure of inconsistency can be given assuming that the amount of of such distance. rework required for changing the battery support size of the me- chanical design to account for the battery size is proportional to Definition 3. (Sequence of ordered points) A sequence of or- the difference in the diameters of the batttery and battery support. dered points (or index on a trace) is a word I = i1 , i2 , ..., in , ... ∈ Thus, the consistency statement can be transformed to provide a N s.t. ∀k, ik < ik+1 . metric for the amount of inconsistency as the difference between Definition 4. (Window) Given a sequence of observations O = the battery and battery support diameters: o1 , o2 , . . . , on , a window w of length λ is defined as a prefix of δ = |ρBatterySize − ρBatterySupportSize | length λ of O. Definition 5. (Trace distance) Given two set of traces Σω 1 and 3.2.2 Vehicle Mass ω For the AGV mass property, we first consider the statements Σ2 generated by two properties ρ1 and ρ2 , respectively, a distance on trace for a given window of lenght λ is a function δλ : Σω 1 × from the viewpoint of the drive train control system VDT C and the Σω 2 7→ M defined as: integrated vehicle mechanical design VIV . In a similar process as λ−1 for the battery support size we derive the consistency statement: X δλ (ρ1 , ρ2 ) = δ(ρ1 (i), ρ2 (i)), ρV ehicleM ass ≤ ρM axV ehicleM assDriveT rainControl i=0 And with similar simplification as for the battery support size prop- where ρ(i) denotes the ith observation of ρ. erty that the amount of rework to account for fixing an inconsistent The above definition can be extended to continuous systems as design is proportional to the difference between the masses, we de- follows: rive the measure: Z λ δλ (ρ1 , ρ2 ) = δ(ρ1 (i), ρ2 (i))di . δ = |ρV ehicleM ass − ρM axV ehicleM assDriveT rainControl | i=0 Definition 6. (Consistency) Two views V1 and V2 are said to be consistent iff 4. TOWARDS TOLERANCE OF INCONSIS- TENCIES ∀ρ ∈ JM KV1 ×V2 : δλ (ρ|V1 , ρ|V2 ) = 0. In this section we discuss how the quantitative model in Section 3 That is, V1 and V2 are consistent iff every property ρ has the same can be used to tolerate semantic inconsistencies. We support the value in both views. notion of two types of inconsistency tolerance. In parameter tolerance, the definition of inconsistency is weak- 4.2 Temporal Tolereance of Inconsistencies ened to allow slight deviations from desired values of parameters, When inconsistencies emerge it may be also desirable to tem- i.e. performance values of semantic properties [49]. In temporal porarily tolerate them, even if the extent of inconsistencies (i.e. the tolerance scenarios, semantic inconsistencies are allowed for a cer- distance between views) exceeds the boundary β as defined pre- tain amount of time before intervening and resolving inconsisten- viously. Temporal tolerance enables reasoning about how long a cies, making use of the fact that inconsistencies might occur, evolve deviation is to be tolerated. For this purpose, we investigate char- and later potentially disappear as the natural consequence of a de- acteristic behavioral patterns of inconsistencies in the temporal di- sign workflow. mension. The patterns can be used in a prescriptive manner, i.e. specifying the expected behavior of properties and consider inter- 4.1 Tolerating Parameter Inconsistencies vention when the expected behavior is not followed. In each pat- The idea of parameter tolerance embraces the presence of slight tern, we assume β-bounded consistency. (See Definition 7.) deviations from desired values of properties while still considering the situation a consistent one. In our specific case this means the 4.2.1 Exact Consistency distance between two views (properties) is not exactly 0, but stays The most simplistic behavioral pattern of properties wrt their within a parameter β. consistency is when the consistency is maintained constantly. Parameter tolerance enables reasoning about how much deviation Definition 8. (Exact consistency) V1 and V2 are exact consistent is to be tolerated. For this purpose, Definition 6 can be weakened for M iff as follows. ∀ρ ∈ JM KV1 ×V2 , ∀t ∈ T : δλt (ρ|V1 , ρ|V2 ) ≤ β. Definition 7. (Bounded consistency) V1 and V2 are β-bounded That is, V1 and V2 are exact consistent iff the consistency is pre- consistent for M iff served constantly, i.e. for every timestamp t∈T. ∀ρ ∈ JM KV1 ×V2 : δλ (ρ|V1 , ρ|V2 ) ≤ β, δ V2 where β is a measure. (See Definition 1.) The above definition V1 allows the distance of two properties being within β, instead of T restricting it to 0. Figure 4: Exact consistency of two views with β = 0. δ V2 +β For our AGV example, this corresponds to the case where the cloud- V1 based multi-view development environment is operating in simulta- −β T neous mode. In such case, the consistency of the properties defined in Table 1 is consistently monitored for each pair of views as the Figure 3: β-bounded consistency of two views. design of the system evolved and immediate resolving actions must be performed in case of any detected inconsistency. In practice, it is however often not efficient to enforce exact From our running example, this occurs for the mass property when consistency during system design, especially in complex multi- a high level of abstraction model of the drive train control system is paradigm and multi-abstraction settings. The following patterns used that, when executed, does not meet real-time deadlines for the formalize cases more likely to be encountered. given inertia due to the mass of the AGV. While the high level of ab- straction model is functionally correct, it does not react fast enough 4.2.2 Eventual Consistency due to poor execution time. The inconsistency with the mass ob- Eventual consistency guarantees that at some point in the future tained from the integrated vehicle view as evaluated according to the two views become consistent. the equation of Section 3.2.2 giving the measure of inconsistency may be tolerated at this level of abstraction up to a given bound β, Definition 9. (Eventual consistency) V1 and V2 are eventually otherwise it is well known by an experienced designer that no im- consistent for M iff plemented system can ever execute fast enough for the given AGV ∀ρ ∈ JM KV1 ×V2 , ∃t ∈ T : δλt (ρ|V1 , ρ|V2 ) ≤ β. inertia. Such parameter inconsistency tolerance is a frequently encoun- δ tered technique in engineering practice, albeit without explicitly obs1 V1 reasoning about it. It is the tacit domain knowledge of stakeholders V2 (engineers) that allows tolerating parameter inconsistencies. The T caveat is, however, that without proper formalizaion, the automa- tion of tolerance mechanisms is not possible. Figure 5: Eventual consistency of two views with β = 0. Contract-Based Design (CBD) [6, 17] can be seen as an enabling methodology to formalize an agreement upon the allowed param- For our AGV example, eventual consistency with β = 0 will be eter tolerances. By defintion, an agreement consists of a set of as- required when the drive train controller design is refined into im- sumptions and guarantees, called a contract, defining under which plementation code and the combined code and execution platform conditions a system promises to operate satisfying desired param- result in meeting the real-time deadlines for the total mass of the eters. Typically, a contract and its content, e.g. the boundaries of AGV. certain parameters, is defined prior to the design phase. When the Demanding eventual consistency is also a typical scenario when relation between parameters is known, e.g. using an ontology [49], parallel branches of design are to be integrated at some point in the one can reason about the tolerated (in)consistency of parameters design process. This leads to the definition of the repetitive and during design. regular consistency patterns presented below. 4.2.3 Repetitive and Regular Consistency more appropriate not to intervene and let inconsistencies exist for Similarly to the eventual case, consistency of views may form a a while. The efficiency of resolution depends on numerous factors, repetitive pattern, i.e. views may be consistent at given points in one of them being the formalisms (i.e. domain-specific languages) time, but may deviate in between. used throughout the process. Some formalisms may support more efficient resolution of a specific type of inconsistencies than others δ and therefore, the analysis of the formalisms used in specific de- obs1 obs2 obs3 obs4 obs5 obs6 obs7 V2 sign steps may help identifying when it is most efficient to address V1 the issue of detected inconsistencies. Richer process models enable T explicit modeling of this information [14], along with the notions of actors and resources of the process [3]. Figure 6: Repetitive consistency of two views. 4.3.2 Specification and Evaluation of Temporal Tol- Definition 10. (Repetitive consistency) V1 and V2 are repetitive erance Rules consistent for M wrt a sequence of ordered points I (see Defini- Specifying temporal tolerance rules makes only sense if those tion 3) iff rules can be evaluated at runtime. Reasoning about temporal struc- tures is traditionally addressed by various forms of temporal logic [24, ∀ρ ∈ JM KV1 ×V2 , ∧i∈I δλ (ρi |V1 , ρi |V2 ) ≤ β. 2, 41], which enable concise proofs and automated theorem proving with off-the-shelf software [29]. In nowadays’ engineering prac- For our AGV example, this corresponds to the case where the de- tice, however, more high-level and domain-specific specification velopment of the different subsystems is subcontracted to external languages are desired. Such languages can be designed in accor- entities and virtual integration steps, at which consistency must be dance with the Dwyer specification patterns [18] for finite-state restored, are planned in advance in an aperiodic manner. verification that occur commonly in the specification of concurrent The repetitive pattern can be more regular w.r.t. to the number and reactive systems. For evaluating temporal tolerance patterns, in the sequence, in this case it means that the index I is such that the techniques of trace matching and complex event processing can ∀i ∈ N, I(i) = τ ∗ i. be used, as presented in previous work [15]. dist 4.3.3 Automation of Tolerance Specification obs1 obs2 obs3 obs4 obs5 obs6 obs7 V2 V1 Tolerance rules applied to single properties usually influence tol- T erance rules of other, related properties. For example, in the run- ning example, the “battery size” is related to the “battery mass” and Figure 7: Regular consistency of two views. inconsistencies between “size” could be also imply inconsistencies in “mass”, which may not be tolerated in the same manner. Manual For our AGV example, this corresponds to the same case as for reasoning about the influence relationships of tolerance rules will repetitive consistency but with periodically planned virtual integra- result in scalability issues in real, industrial-sized models. Automa- tion phases. tion of specifying tolerance rules is, therefore, a critical require- ment for an efficiently tolerating inconsistencies. Combinatorial 4.3 Discussion optimization techniques and design-space exploration can aid the The quantification approach of semantic inconsistencies described process of tolerance specification, and can provide a mechanism in this paper serves as foundations for a comprehensive inconsis- for exploring incompatible tolerance rules. tency tolerance approach that can be adopted in state-of-the-art consistency management frameworks. Our work focuses on two 4.3.4 Predictive Impact Analysis types of inconsistency tolerance: parameter inconsistency tolerance The real challenge of answering whether or not to intervene at and temporal tolerance in general. a specific point of the design process to resolve inconsistencies, is Toleration methods for parameter inconsistencies can be directly to understand how the inconsistencies can evolve in the subsequent implemented based on the theory described in Section 4.1. A re- steps of the process. Inconsistency resolution should be carried out quirement to such methods is the explicit notion of semantic traces, only if the views are potential subjects of further diverging, but it which can be achieved by explicit modeling of operational seman- should be postponed if the views can converge as a result of sub- tics, described e.g. in [16, 51]. sequent activities. With respect to the quantified distance metric, In the following, we discuss the required extensions and future this raises the need for predictive techniques to be incorporated in directions to the current results to make the foundations of temporal our distance models to estimate how the impact of an inconsistency tolerance described in Section 4.2 applicable in complex collabo- can evolve. In its most simplistic form, techniques of time series rative modeling settings. analysis can be employed [11]. In more complex scenarios, the propagation of inconsistencies may be required to be predicted too. 4.3.1 Explicitly Modeled Processes Explicitly modeled processes enable various analyses required 4.3.5 Resolution Scheduling for reasoning about temporarily tolerating inconsistencies. First, Another important cost-related factor is the resolution schedul- they depict how models evolve throughout the development. The ing strategy of inconsistencies. Mens et al [35] investigated how a precedence relationships between various activities modifying the small number of inconsistencies can lead to hard resolution schedul- models are made clear, which helps understanding where and how ing problems, including cyclic dependencies between inconsisten- inconsistencies occur exactly. cies, which make naïve resolution techniques fail. Consequently, Deciding whether to resolve an inconsistency or further tolerate the analysis of resolution plans is important to understand the fea- it, eventually depends on the added value a fixed inconsistency car- sibility of resolution and provides essential information on whether ries. If the cost of resolving an inconsistency is high, it may be or not to execute resolution at the given time of the process. 4.3.6 Proving Global (In)Consistency et al [33] use the number of detected instances of various incon- Proving the consistent (or inconsistent) state of the models is a sistency rules between UML diagrams as an inconsistency metric natural extension of the quantification model. By evaluating lo- between views. Inconsistency rules are syntactic, such as messages cal consistency and defining the algebraic rules of composition of in sequence diagrams without names. views [6], information about the global consistency can be inferred Similar to our approach is the one presented by Barragáns-Martínez in an automated fashion. Apart from the composition rules of views, et al [5], who provide a formal framework to assess the significance proving global (in)consistency depends on how the semantic do- of inconsistencies in requirement specifications. The scope of our mains of views overlap as discussed in [37]. work is more general as our technique is not constrained to require- ment specifications but arbitrary models in a collaborative setting. 5. RELATED WORK 5.3 Temporal Tolerance 5.1 Inconsistency Management Balzer et al [4] introduces the notion of temporal tolerance by Managing inconsistencies has been a well-studied topic in the deconstructing inconsistency rules to two derived rules, the appear- domain of software engineering [46]. With the advent of complex ance and disappearance rule which span a temporal interval of the engineered systems that require collaborative model development, model(s) being in an inconsistent state, hence making inconsisten- addressing the topic of inconsistencies in a multi-view context be- cies stateful entities. By allowing further engineering activities to came more relevant. Persson et al [37] identify consistency be- be executed during the inconsistent interval, the better paralleliza- tween the various views of cyber-physical system design as one of tion of the design workflow can be achieved and ultimately, these the main challenges in design of such complex systems. The out- may lead to the inconsistencies to be resolved without interrupt- look to the near-future of multi-view modeling by Hanxleden et ing the design process for further reconciliation. As a limitation, al [50] further emphasizes the need for inconsistency management the technique only deals with the most simplistic version of tempo- techniques in distributed, agile development settings with global- ral consistency relations, in which a pair of subsequent operations ized DSLs and actor-oriented cloud based modeling tools. form an identity transformation. In practice, more complex struc- Traditional approaches focus on maintaining consistency on the tures of operations have to be supported. linguistic level, typically employing some form of correspondence Easterbrook et al [19] propose a framework for temporal incon- models, such as dependency graphs [25, 26] and pivot models, e.g. sistency tolerance in the context of multi-view modeling. Tolerat- by using SysML [44, 43] or EAST-ADL [8]. Qamar et al [38] ing inconsistencies decouples the viewpoints and introduces flex- introduce an inconsistency management approach by explicit mod- ibility in the design process as deciding upon when to resolve in- eling of inter- and intra-model dependencies. Dependencies are di- consistencies is the responsibility of the owner of the view. The au- rect results of semantic overlaps and are used to notify stakeholders thors provide a formal approach for guiding the decision in form of about possible inconsistencies when dependent properties change. pairs of pre- and postconditions. Our approach extends this model Adourian et al [1] use triple-graph grammars (TGG) for maintain- by using a quantifiable distance metric to evaluate the divergence ing consistency between geometric and dynamic properties of me- of views (and viewpoints). The distance metric also helps under- chanical systems. Bhave et al [9] use an architectural base model as standing the impact of unresolved inconsistencies and reason over a pivot model and a set of model transformations for bi-directional their accumulation and evolution. mapping between various views and the base model. As opposed to our work, the above techniques do not consider 5.4 Consistency in Other Contexts inconsistencies of purely semantic nature, i.e. the ones that do Consistency issues are of course well known in distributed and not manifest on the syntactic level. Multiple works focus on ef- multiprocessor contexts, where program correctness is strongly de- ficiently expressing semantic and ontological properties. Hehen- pendent on understanding precise conditions under which the mem- berger et al [28] relate semantic concepts to the linguistic concepts ories of different processors may differ. Lamport’s seminal work on of modeling by organizing structural design elements and their re- parallel computers, for instance, developed core notions of consis- lations into a domain ontology to identify inconsistencies. Chechik tency as preserving causality between events [31], or in terms of et al [12] introduce the notion of approximate properties: linguistic interleaving sequential streams in the well known Sequential Con- properties expressed as graph patterns which are accurate enough sistency model [32]. A wide variety of less strict, or “relaxed” con- to appropriately approximate a semantic property. These works can sistency models have since been defined, although they are often serve as complementary techniques to our work, to provide the se- quite specific to the design decisions made in the underlying hard- mantic properties our technique can be applied on. ware [42]; Sorin et al.’s book provides a good overview [45] of memory model designs and issues. 5.2 Measuring Inconsistency A number of approaches to categorizing consistency have also Measuring inconsistency has been a topic of interest in the on- been attempted. For distributed, virtual environments, Bouillot and tology and knowledge engineering. Hunter and Konieczny [30] ap- Gressier-Soudan decompose consistency into elements of causal- proach measuring the level of inconsistency through the notion of ity, concurrency, simultaneity, and instantaneity [10]. The latter 2 minimal inconsistency sets. They show how their inconsistency are difficult to achieve, and typically imply sacrificing the former 2 metric is a special Shapley Inconsistency Value, which enables us- and living with short-term inconsistencies. Liu et al.’s survey paper ing SAT techniques for proving consistency and inconsistency. Ma organizes models based on their focus on ultimate consistency (sys- et al [34] propose a technique to measure the degree of inconsis- tems which become eventually consistent), or on being deadline- tency in description logic based ontologies. As compared to these based (given an event at time t, consistency is achieved at t + δ). approaches, we mainly focus on collaborative modeling of com- The former includes Lamport’s basic models, as well as various plex engineered systems where the semantic inconsistencies of the similar forms of serializability [7], while the latter can be further models are not that obvious as in ontologies. broken down into perceptive (or absolute) consistency [10], where Inconsistency measurement approaches in software engineering every process executes events at the same absolute time, delayed settings typically focus on inconsistencies on linguistic level. Lange consistency [39], which imposes a fixed, maximum pair-wise delay of δ(i, j) between processes i and j, and timed consistency [48], Systems Design : Theory. Technical Report RR-8759, which requires a fixed global bound of δ on all processes. In this INRIA, 2015. terminology our definition of eventual consistency is an instance of [7] P. A. Bernstein, V. Hadzilacos, and N. Goodman. ultimate consistency, exact consistency a kind of absolute consis- Concurrency Control and Recovery in Database Systems. tency, and regular consistency is deadline-based. Repetitive con- Addison-Wesley Longman Publishing Co., Inc., Boston, sistency and bounded consistency introduce new ideas based on a MA, USA, 1987. flexible notion of delay, and a formal distance metric for relative [8] A. Bhave, B. Krogh, D. Garlan, and B. Schmerl. consistency. Multi-domain modeling of cyber-physical systems using architectural views. The First Analytic Virtual Integration of 6. CONCLUSION Cyber-Physical Systems Workshop, pages 43–50, 2010. In this paper, we presented a quantification model for semantic [9] A. Bhave, B. H. Krogh, D. Garlan, and B. Schmerl. View inconsistencies in multi-view settings of collaborative system de- consistency in architectures for cyber-physical systems. In sign. The model serves as the foundation of a more comprehensive Proceedings - 2011 IEEE/ACM 2nd International inconsistency tolerance methodology. By elaborating on character- Conference on Cyber-Physical Systems, pages 151–160, istic examples we concluded that the model is well-suited for sup- 2011. porting the notion of parameter inconsistency tolerance and also [10] N. Bouillot and E. Gressier-Soudan. Consistency models for tolerating inconsistencies in the temporal aspect. distributed interactive multimedia applications. SIGOPS This paper reported the results of a work in progress and there- Operating Systems Review, 38(4):20–32, Oct. 2004. fore, the links to the state-of-the-art have been explored, as well as [11] G. Box, G. Jenkins, and G. Reinsel. Time Series Analysis: the further directions to be investigated. One particularly important Forecasting and Control. Wiley Series in Probability and direction concerns the measure of level of inconsistency. Our sim- Statistics. Wiley, 2008. plified example measures need to be extended to include a study on [12] M. Chechik, F. Dalpiaz, C. Debreceni, J. Horkoff, I. Ráth, how to relate a measure of inconsistency with the cost of fixing it R. Salay, and D. Varró. Property-Based Methods for given an actual design, the other dependent consistency properties Collaborative Model Development. In Proc. of 3rd Int. and their dependency graph, and given an inconsistency resolution Workshop on The Globalization of Modeling Languages plan expressed as a sequence of activities to be performed on the (GEMOC 2015), 2015. involved views. Adequate modeling of all these artifacts and cor- [13] J. Corley, E. Syriani, H. Ergin, and S. Van Mierlo. responding analysis methods will be required to better support this Cloud-based multi-view modeling environments. In Modern task. Software Engineering Methodologies for Mobile and Cloud Environments. IGI Global, 2015. Acknowledgments [14] I. Dávid, J. Denil, and H. Vangheluwe. Towards inconsistency management by process-oriented dependency This work has been partially carried out within the MBSE4Mechatronics modeling. In Proceedings of 9th International Workshop on project (grant nr. 130013) of the Flanders Innovation & Entrepreneur- Multi-Paradigm Modeling, pages 32–41, 2015. ship agency (VLAIO). This research was partially supported by [15] I. Dávid, I. Ráth, and D. Varró. Foundations for streaming Flanders Make vzw. model transformations by complex event processing. The authors would like to express their gratitude to the organiz- Software & Systems Modeling, pages 1–28, 2016. ers of the Computer Automated Multi-Paradigm Modelling work- shop (CAMPaM) where the foundations of this work have been [16] J. de Lara and H. Vangheluwe. AToM3: A Tool for carried out. Multi-formalism and Meta-modelling. In R.-D. Kutsche and H. Weber, editors, Fundamental Approaches to Software Engineering: 5th International Conference, FASE 2002 Held 7. REFERENCES as Part of the Joint European Conferences on Theory and [1] C. Adourian and H. Vangheluwe. Consistency between Practice of Software, ETAPS 2002 Grenoble, France, April geometric and dynamic views of a mechanical system. In 8–12, 2002 Proceedings, pages 174–188. Springer Berlin Proceedings of the 2007 Summer Computer Simulation Heidelberg, Berlin, Heidelberg, 2002. Conference, SCSC ’07, pages 31:1–31:6, San Diego, CA, [17] P. Derler, E. A. Lee, S. Tripakis, and M. Törngren. USA, 2007. Society for Computer Simulation International. Cyber-Physical System Design Contracts. In ICCPS ’13, [2] J. F. Allen. Maintaining knowledge about temporal intervals. pages 109–118. ACM, 2013. Communications of the ACM, 26(11):832–843, 1983. [18] M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Property [3] C. Artigues, S. Demassey, and E. Neron. specification patterns for finite-state verification. In Resource-Constrained Project Scheduling: Models, Proceedings of the second workshop on Formal methods in Algorithms, Extensions and Applications. ISTE, 2007. software practice, pages 7–15. ACM, 1998. [4] R. Balzer. Tolerating inconsistency. In 13th International [19] S. Easterbrook, A. Finkelstein, J. Kramer, and B. Nuseibeh. Conference on Software Engineering, pages 158–165, 1991. Coordinating distributed viewpoints: the anatomy of a [5] B. Barragáns-Martínez, J. Pazos-Arias, and consistency check. Concurrent Engineering, 2(3):209–222, A. Fernández-Vilas. On measuring levels of inconsistency in 1994. multi-perspective requirements specifications. In [20] C. Ericson. Real-time collision detection. CRC Press, 2004. Proceedings of the 1st Conference on the Principles of [21] A. Finkelstein. A foolish consistency: Technical challenges Software Engineering (PRISE’04), pages 21–30, 2004. in consistency management. In M. Ibrahim, J. Küng, and [6] A. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J.-B. N. Revell, editors, Database and Expert Systems Raclet, P. Reinkemeier, A. Sangiovanni-Vincentelli, Applications, volume 1873 of Lecture Notes in Computer W. Damm, T. Henzinger, and K. G. Larsen. Contracts for Science, pages 1–5. Springer Berlin Heidelberg, 2000. [22] A. C. W. Finkelstein, D. Gabbay, A. Hunter, J. Kramer, and Selected Papers, pages 111–126. Springer Berlin Heidelberg, B. Nuseibeh. Inconsistency handling in multiperspective Berlin, Heidelberg, 2007. specifications. IEEE Transactions on Software Engineering, [36] G. Moroni, T. Tolio, S. J. I. Herzig, and C. J. J. Paredis. A 20(8):569–578, Aug 1994. conceptual basis for inconsistency management in [23] R. France and B. Rumpe. Model-driven development of model-based systems engineering. Procedia CIRP, complex software: A research roadmap. In L. Briand and 21:52–57, 2014. A. L. Wolf, editors, Future of Software Engineering, pages [37] M. Persson, M. Törngren, A. Qamar, J. Westman, M. Biehl, 37–54, Minneapolis, may 2007. IEEE Computer Society. S. Tripakis, H. Vangheluwe, and J. Denil. A characterization [24] D. M. Gabbay, I. Hodkinson, and M. Reynolds. Temporal of integrated multi-view modeling in the context of logic mathematical foundations and computational aspects. embedded and cyber-physical systems. In Proceedings of the 1994. International Conference on Embedded Software, 2013. [25] J. Gausemeier, W. Schäfer, J. Greenyer, S. Kahl, S. Pook, [38] A. Qamar, C. J. Paredis, J. Wikander, and C. During. and J. Rieke. Management of cross-domain model Dependency modeling and model management in consistency during the development of advanced mechatronic design. Journal of Computing and Information mechatronic systems. In DS 58-6: Proceedings of ICED 09, Science in Engineering, 12(4), 2012. the 17th International Conference on Engineering Design, [39] X. Qin. Delayed consistency model for distributed interactive Vol. 6, Design Methods and Tools (pt. 2), Palo Alto, CA, systems with real-time continuous media. Journal of USA, 24.-27.08.2009, pages 1–12, 2009. Software, 6(13):1029–1039, 2002. [26] H. Giese and S. Hildebrandt. Incremental model [40] J. Reineke and S. Tripakis. Basic problems in multi-view synchronization for multiple updates. In Proceedings of the modeling. In Tools and Algorithms for the Construction and Third International Workshop on Graph and Model Analysis of Systems, volume 8413 of LNCS, pages 217–232. Transformations, GRaMoT ’08, pages 1–8, New York, NY, Springer, 2014. USA, 2008. ACM. [41] G. Roşu and S. Bensalem. Allen linear (interval) temporal [27] J. Grundy, J. Hosking, and W. B. Mugridge. Inconsistency logic–translation to ltl and monitor synthesis. In management for multiple-view software development International Conference on Computer Aided Verification, environments. IEEE Transactions on Software Engineering, pages 263–277. Springer, 2006. 24(11):960–981, Nov 1998. [42] P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. [28] P. Hehenberger, A. Egyed, and K. Zeman. Consistency Myreen. x86-TSO: A rigorous and usable programmer’s checking of mechatronic design models. In 30th Computers model for x86 multiprocessors. Communications of the and Information in Engineering Conference, volume 3: Parts ACM, 53(7):89–97, 2010. A and B, pages 1141–1148. ASME, 2010. [43] A. A. Shah, A. A. Kerzhner, D. Schaefer, and C. J. J. Paredis. [29] P. Höfner. How to find algebraic semantics for modal and Multi-view modeling to support embedded systems temporal logics. https://www.informatik.uni-augsburg.de/ engineering in sysml. In G. Engels, C. Lewerentz, lehrstuehle/dbis/pmi/alumni/hoefner/talks/09_relmics/. W. Schäfer, A. Schürr, and B. Westfechtel, editors, Graph Invited talk at the 11th International Conference on Transformations and Model-driven Engineering, pages Relational Methods in Computer Science / 6th International 580–601. Springer-Verlag, Berlin, Heidelberg, 2010. Conference on Applications of Kleene Algebra [44] A. A. Shah, D. Schaefer, and C. J. J. Paredis. Enabling (RelMiCS11/AKA6). Accessed: 2016-08-30. multi-view modeling with sysml profiles and model [30] A. Hunter, S. Konieczny, et al. Measuring inconsistency transformations. In International Conference on Product through minimal inconsistent sets. KR, 8:358–366, 2008. Lifecycle Management, pages 527–538, 2009. [31] L. Lamport. Time, clocks, and the ordering of events in a [45] D. J. Sorin, M. D. Hill, and D. A. Wood. A primer on distributed system. Communications of the ACM, memory consistency and cache coherence. Number 16 in 21(7):558–565, July 1978. Synthesis Lectures on Computer Architecture. Morgan & [32] L. Lamport. How to make a multiprocessor computer that Claypool, 2011. correctly executes multiprocess programs. IEEE [46] G. Spanoudakis and A. Zisman. Inconsistency management Transactions on Computers, 28(9):690–691, Sept. 1979. in software engineering: Survey and open research issues. In [33] C. Lange, M. R. V. Chaudron, J. Muskens, L. J. Somers, and in Handbook of Software Engineering and Knowledge H. M. Dortmans. An empirical investigation in quantifying Engineering, pages 329–380. World Scientific, 2001. inconsistency and incompleteness of uml designs. In [47] M. Törngren, A. Qamar, M. Biehl, F. Loiret, and Incompleteness of UML Designs, Proc. Workshop on J. El-khoury. Integrating viewpoints in the development of Consistency Problems in UML-based Software Development, mechatronic products. Mechatronics, 24(7):745 – 762, 2014. 6 th International Conference on Unified Modeling 1. Model-Based Mechatronic System Design 2. Model Based Language, UML 2003, 2003. Engineering. [34] Y. Ma, G. Qi, P. Hitzler, and Z. Lin. Measuring Inconsistency [48] F. J. Torres-Rojas, M. Ahamad, and M. Raynal. Timed for Description Logics Based on Paraconsistent Semantics, consistency for shared distributed objects. In Proceedings of pages 30–41. Springer Berlin Heidelberg, Berlin, the Eighteenth Annual ACM Symposium on Principles of Heidelberg, 2007. Distributed Computing, PODC ’99, pages 163–172, New [35] T. Mens and R. Van Der Straeten. Incremental resolution of York, NY, USA, 1999. ACM. model inconsistencies. In J. L. Fiadeiro and P.-Y. Schobbens, [49] K. Vanherpen, J. Denil, I. Dávid, P. De Meulenaere, P. J. editors, Recent Trends in Algebraic Development Mosterman, M. Törngren, A. Qamar, and H. Vangheluwe. Techniques: 18th International Workshop, WADT 2006, La Ontological reasoning for consistency in the design of Roche en Ardenne, Belgium, June 1-3, 2006, Revised cyber-physical systems. In 2016 1st International Workshop on Cyber-Physical Production Systems (CPPS), pages 1–8, April 2016. [50] R. von Hanxleden, E. A. Lee, C. Motika, and H. Fuhrmann. Multi-view modeling and pragmatics in 2020. In R. Calinescu and D. Garlan, editors, Large-Scale Complex IT Systems. Development, Operation and Management, volume 7539 of Lecture Notes in Computer Science, pages 209–223. Springer Berlin Heidelberg, 2012. [51] G. Wachsmuth. Modelling the operational semantics of domain-specific modelling languages. In R. Lämmel, J. Visser, and J. Saraiva, editors, Generative and Transformational Techniques in Software Engineering II: International Summer School, GTTSE 2007, Braga, Portugal, July 2-7, 2007. Revised Papers, pages 506–520. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008.