Formalizing Cyber--Physical System Model Transformation via Abstract Interpretation

TL;DR

This paper introduces a formal, sound approach to model transformation in cyber-physical systems using abstract interpretation, enabling consistent and domain-agnostic system modeling.

Contribution

It develops a foundational methodology for model transformation based on abstract interpretation, with formal proofs of correctness and domain transfer capabilities.

Findings

Proves soundness of the abstract interpretation-based transformation

Defines formalism for encoding model properties

Demonstrates cross-domain applicability of the approach

Abstract

Model transformation tools assist system designers by reducing the labor--intensive task of creating and updating models of various aspects of systems, ensuring that modeling assumptions remain consistent across every model of a system, and identifying constraints on system design imposed by these modeling assumptions. We have proposed a model transformation approach based on abstract interpretation, a static program analysis technique. Abstract interpretation allows us to define transformations that are provably correct and specific. This work develops the foundations of this approach to model transformation. We define model transformation in terms of abstract interpretation and prove the soundness of our approach. Furthermore, we develop formalisms useful for encoding model properties. This work provides a methodology for relating models of different aspects of a system and for applying modeling techniques from one system domain, such as smart power grids, to other domains, such as water distribution networks.

Equations

$$(\gamma \circ \alpha )(p)$$

$$(\alpha \circ \gamma )(m)$$

$$s{R}_{\text{StrLeft}\mathbb{M}1\text{StrGobbleLeft}\mathbf{M}1}{m}_1\wedge m_1⊑m_2$$

$$⟺$$

$$⟹$$

$$⟺$$

$$\forall m\in {\mathbf{M}}^{\prime }s{R}_{\text{StrLeft}\mathbb{M}1\text{StrGobbleLeft}\mathbf{M}1}m$$

$$⟺$$

$$⟹$$

$$⟺$$

$$s{R}_{\text{StrLeft}{\mathbb{M}}_{1}1\text{StrGobbleLeft}{\mathbf{M}}_{1}1}{m}_1$$

$$⟺$$

$$⟹$$

$$⟺$$

$$f\bigsqcup g$$

$$f\sqcap g$$

$${\varphi }_A^B(f):=\lambda t.\{\begin{array}{ll}f(t)& \text{if }t\in \mathbf{A}\cap \mathbf{B}\\ \mathbf{O}& \text{if }t\in \mathbf{B}-\mathbf{A}\end{array}$$

$${\varphi }_A^B(f)=\{(t,\mathbf{o})\in f\mid t\in \mathbf{A}\cap \mathbf{B}\}\cup \{(t,\mathbf{O})\mid t\in \mathbf{B}-\mathbf{A}\}$$

$$\displaystyle\phi_{A}^{B}\left(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}\mathbf{O^{\prime}}\right)(t)$$

$$=$$

$$\displaystyle\phi_{A}^{B}\left(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}\mathbf{O^{\prime}}\right)(t)$$

$$=$$

$$({\mathbf{T}}_1,f)\sqcap ({\mathbf{T}}_2,g)$$

$$=$$

$$\sqcap \{(t_1,\mathbf{O}),(t_2,\{x\}),(t_3,\{y\})\})$$

$$=$$

$$\forall l\in \mathbf{\Lambda },(T^{\prime },f^{\prime })⊑l$$

$$⟹$$

$$($$

Full text

I Introduction

The multitude of functional and non–functional requirements for critical infrastructure cyber–physical systems (CPSs) present many challenges to system designers. A smart grid must be able to supply all its customers; it must be fault–tolerant in the face of component failure; it must be secure against physical and cyber attacks; and it must achieve all these goals with efficient infrastructure. To meet all these requirements, designers must integrate physical components, cyber control software and hardware, and processes for human operators into a complete system. This is a truly daunting task, but one that can be facilitated by model-based design and evaluation.

A vast body of literature has been published on various modeling formalisms that capture system performance, dependability, safety, and security. No single modeling formalism can encompass all aspects of system performance and dependability, necessitating the labor–intensive and error–prone process of creating multiple system models and propagating changes across all of these models. Furthermore, designers must be careful that these models remain consistent with each other, i.e., that the assumptions made about the system by one model are not contradicted by those of any other model. For instance, a dependability model for a smart grid where two power lines are assumed to be connected in parallel is not compatible with a power flow analysis where the lines are placed in series.

One way to alleviate these challenges is through model transformation, which enables automated or semi-automated transformations between modeling formalisms. These transformations can ensure that modeling assumptions are consistent across every model of a system by verifying that any model can be transformed into any other. This approach can also identify constraints on system design imposed by these assumptions. Such a model transformation approach should meet two design constraints. First, it should be applicable to a broad range of systems and a variety of modeling formalisms in order to be useful to designers of complex systems. Second, it should be sound—it should be possible to prove that the result of a transformation is correct and consistent with the initial models.

In our earlier work [1], we proposed a model transformation approach based on abstract interpretation, a static program analysis technique. Models are seen as abstractions of the semantics of a system—its structure and behavior. Through this lens, provably correct model transformation becomes the problem of defining sound mappings from system semantics to model semantics and vice versa. By composing these mappings, we can develop sound transformations between modeling formalisms.

The research contribution of this work is twofold. We propose:

a formalization of system and model semantics, leading to a formalization of sound model transformation, and 2. 2.

a mathematical structure useful in the development of structures that capture system semantics.

Our first contribution formalizes the research approach we outlined in [1] and incorporates several improvements from feedback we have received since publication of that work. The second contribution lays the groundwork for integrating real–world modeling formalisms into this model transformation approach.

The structure of this paper is as follows: in Section II, we briefly summarize related model transformation and formalization techniques. Section III presents our formalization of system and model semantics and describes how we use this formalization to create a method for model transformation. Section IV presents tag–option lattices, a structure that we find to be useful when formalizing the semantics of systems. Section V summarizes our work and discusses future directions for our research.

II Related Work

In the literature, model transformation refers to two different but related concerns. One concern is integrating models of different parts of the system into a complete system model; this is more specifically called * heterogeneous model composition*. The other concern is transforming one type of model for a system to a different model of the same system or a related system.

Model transformation research specific to CPSs primarily focuses on building hierarchical models [2, 3, 4, 5]. Hierarchical models allow different model types to be combined together to model complex systems. Each component can be modeled in a convenient formalism; the hierarchical model is then simulated by simulating each sub-model in tandem.

The Ptolemy modeling software [6] performs hierarchical modeling and model composition [7, 8]. As such, Ptolemy makes it easy to build and link small models. Hierarchical models can consist of heterogeneous sub–models, allowing different parts of the system to be expressed using different types of models [9, 10, 11, 8]. Model composition is achieved in part by defining ontologies of system properties, e.g., units of model inputs and outputs. Based on these ontologies, Ptolemy can perform conversions of values transmitted between sub–models and check for incompatibilities which indicate modeling errors. Ptolemy also enables heterogeneous model evaluation: it provides choices for both the modeling language and the solution or simulation technique used to evaluate the model [12]. However, Ptolemy does not offer methods for transforming one system–level model to another. In addition, it is focused on models of system function and lacks facilities for modeling non-functional attributes.

OsMoSys [13] and SIMTHESys [14] are modeling systems motivated by model–driven engineering. Their approach to model transformation is based on techniques from software engineering. Graph–based models, such as Petri Nets and Fault Trees, are described using an object–oriented notation. Every model has associated interfaces which allow models of different types to be composed and evaluated. OsMoSys features compositional models and interfaces with external tools to evaluate them [15]. SIMTHESys provides a language in which users can describe new modeling formalisms for use with OsMoSys. Both are capable of modeling both functional and non-functional aspects of a system [16]. However, neither are focused on the problem of model transformation.

Möbius [17] is another modeling tool that supports hierarchical modeling. It supports several modeling formalisms, including block diagrams and Petri nets, and additional formalisms including stochastic timed systems can be included via external modeling tools [18, 19]. While this feature offers considerable flexibility in modeling, Möbius is constructed around a modeling workflow that builds and evaluates hierarchical models and has little support for model transformation. Its model composition method is based on object–oriented design principles and is applicable to many state–based model formalisms.

AToM3 [20] is capable of both model transformation and model composition. It uses metamodels to describe specific modeling languages, then defines transformations between metamodels to transform models [21]. Models are graph-based and transformations take the form of graph rewriting rules [22]. However, there is no hierarchy of models, so introducing a new model requires writing transformation rules from the new model to each model that AToM3 implements.

CHESS [23] provides a modeling language for describing systems and includes several model transformation methods specific to creating dependability models. CHESS is based on the Unified Modeling Language (UML); transformations are based on graph rewriting rules. CONCERTO [24] extends CHESS by introducing modeling techniques for non-functional system attributes such as dependability [25]. However, CONCERTO is focused on multicore processing systems [26, 27] and lacks the features necessary for modeling complex physical components.

Rosetta [28] is focused on functional multi–formalism modeling [29]. It takes an algebraic approach to relating models: each formalism is described as a coalgebra—a mathematical system useful for describing arbitrary transitions among arbitrary states [30, 31]. The coalgebras corresponding to each formalism are placed in a lattice, which provides a structure for determining how to transform one model into another. Model transformations can be used to relate different models of the same system; for example, it is possible to combine a functional system model with a model of that system’s power consumption. However, Rosetta lacks many features required for CPS modeling, especially support for hybrid discrete–continuous formalisms.

Each of these model transformation tools offers a partial solution to the model transformation problem; however, none of them present a solution that is generally applicable. Some frameworks place constraints on the behavior of transformation functions (e.g., class inheritance transformation). Others apply only to specific formalisms. Furthermore, only Rosetta offers an approach that can be proven to be correct. The work presented in this paper aims to address these shortcomings by providing a model transformation approach that relates a wide variety of modeling formalisms in a provably sound fashion, and yields results that are sufficiently specific to be meaningful.

III Abstract Interpretation of Models

The foundation of our approach is abstract interpretation [32, 33], a formalism for developing sound semantic abstractions. In this work, system semantics are represented in terms of properties that hold for the system. Such properties might include information about components, their reliabilities, and how they are interconnected. Models are abstractions of system semantics—they concern certain properties of the system, but not others. Thus, generating a model from a system’s properties, then deriving properties of that system from the generated model, may result in some of the initial properties not being present in the derived properties. This is a necessary effect of abstraction—we cannot derive properties from a model if the model does not capture those properties. To define mappings from system properties to models and vice versa, both domains need to allow for this potential loss of precision.

III-A Properties

We first define how system semantics are represented. Lattices (see [34]) offer a useful formalism for describing the nature of approximation. We define a complete $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ lattice ordered by specificity: for $p_{1},p_{2}\in\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}},p_{1}\sqsubseteq p_{2}$ means that the constraints in $p_{1}$ and $p_{2}$ are not contradictory and that $p_{1}$ places the same or more constraints on a system than $p_{2}$ does. For example, $p_{2}$ could constrain the reliability of a component to fall in the range $(0,1]$, whereas $p_{1}$ could require that component to have a reliability of $0.95$.

The meet (denoted as $\sqcap$) of two elements of $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ places the constraints of both elements on a system; the join (denoted as $\sqcup$) implies satisfaction of the constraints of either element. Suppose $p_{1}$ requires a component’s reliability to fall in $[0.8,1.0]$ and $p_{2}$ constrains it within $[0.75,0.9]$. Then $p_{1}\sqcap p_{2}$ will require it to be in $[0.8,0.9]$ and $p_{1}\sqcup p_{2}$ within $[0.75,1.0]$. \mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}} and $\bigsqcup$ extend this concept to subsets of $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$.

For certain $p_{1},p_{2}\in\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ are contradictory, $p_{1}\sqcap p_{2}$ will result in a constraint that is impossible to satisfy. If $p_{1}$ requires a component to have a reliability in $[0.5,0.7]$ and $p_{2}$ requires it in $[0.9,1]$, then it is impossible for any component to meet both constraints. In this paper, we require that every element of $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ to be satisfiable except for $\bot$, the “impossible” constraint. Therefore, for this example, $p_{1}\sqcap p_{2}=\bot$. Note that $\forall p\in\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}},\bot\sqsubseteq p$.

To summarize, each element of the $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ lattice describes one or more systems. In the general case, $p$ describes a set of systems, all of which meet the constraints in $p$. If every constraint in $p\in\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ has exactly one possible choice, $p$ will describe a single system.

III-B Models

We now consider how modeling formalisms can be represented in this lattice framework. As a given element of the $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ lattice may not define a single system, we must account for the possibility that the lattice may not specify the system well enough for a single model to be abstracted from it. If $p\in\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ does not constrain the reliability of a component to a single value, a single reliability model cannot be abstracted from $p$. Instead, we abstract a set of models, one for each possible assignment of the component’s reliability, subject to the constraints of $p$.

Therefore, in the same way that the $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ lattice is defined, we also define the domain of each modeling formalism to account for the nature of potentially imprecise system specifications. To ensure that this approach is broadly applicable, we define this domain using structure external to the modeling formalism itself. Thus we do not have to require, say, that a reliability model formalism be able to express the concept of a component having a range of possible reliabilities.

We use a powerset lattice to provide this extra structure. For a given model formalism, the set $\mathbf{Model}$ contains all possible models expressible in that formalism. The powerset lattice $\mathcal{P}(\mathbf{Model})$ then forms a lattice ordered by specificity: for $M_{1},M_{2}\subseteq\mathbf{Model}$, $M_{1}\subseteq M_{2}$ indicates that $M_{1}$ contains fewer possible models describing a system, and thus places more constraints on the system, than $M_{2}$ does. Likewise, $M_{1}\cap M_{2}$ produces a set of models that fit the constraints associated with $M_{1}$ and with $M_{2}$; $M_{1}\cup M_{2}$ produces a set of models where constraints from either may hold.

Singleton sets (i.e., sets of the form $\{m\}$, $m\in\mathbf{Model}$) correspond to fully-specified models, and $\emptyset=\bot$ corresponds to an “impossible” system—one with contradictory modeling requirements.

To make the notation clearer and more consistent, we will define $\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}=\mathcal{P}(\mathbf{Model})$, as the powerset lattice of the original set of models, $\mathbf{Model}$ . For the powerset lattice $\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}$, we will use the rounded operators ($\subseteq,\bigcap,\bigcup$) to prevent confusion with the square operators of the lattice $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$, and of lattices in the abstract.

III-C Correctness

In this work, we represent the set of systems by $\mathcal{S}$. We think of these systems abstractly; thus, we do not concern ourselves with the representation of $\mathcal{S}$ or its elements. When we speak of a system $s\in\mathcal{S}$, we understand $s$ to be the system to be modeled.

Any system $s\in\mathcal{S}$ is described by a number of elements of $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$. To formalize this notion, we use a correctness relation to relate a system to properties (and later, models) that describe it. We suppose a relation $R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}:\mathcal{S}\rightarrow\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ where $s\,R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}\,p$ if and only if $p$ describes the system $s$. We must assume the existence of $R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}$, since the properties of the system being designed are determined by the designer. However, abstract interpretation allows us to induce correctness relationships between systems and models based on $R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}$—in other words, abstract interpretation enables sound transformations between system properties and system models.

Definition III.1

A correctness relation $R_{\mathbb{\StrLeft{L}{1}}\mathbf{\StrGobbleLeft{L}{1}}}:\mathcal{S}\rightarrow\mathbb{\StrLeft{L}{1}}\mathbf{\StrGobbleLeft{L}{1}}$ relates systems to elements of a lattice $\mathbb{\StrLeft{L}{1}}\mathbf{\StrGobbleLeft{L}{1}}$. Two attributes hold for $R_{\mathbb{\StrLeft{L}{1}}\mathbf{\StrGobbleLeft{L}{1}}}$:

1. (i)

If $s\,R_{\mathbb{\StrLeft{L}{1}}\mathbf{\StrGobbleLeft{L}{1}}}\,l_{1}$ and $l_{1}\sqsubseteq l_{2}$, then $s\,R_{\mathbb{\StrLeft{L}{1}}\mathbf{\StrGobbleLeft{L}{1}}}\,l_{2}$. 2. (ii)

If $\forall l\in\mathbf{L^{\prime}}\subseteq\mathbb{\StrLeft{L}{1}}\mathbf{\StrGobbleLeft{L}{1}},s\,R_{\mathbb{\StrLeft{L}{1}}\mathbf{\StrGobbleLeft{L}{1}}}\,l$, then s\,R_{\mathbb{\StrLeft{L}{1}}\mathbf{\StrGobbleLeft{L}{1}}}\,\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{L^{\prime}}.

In terms of $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ and its correctness relation $R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}$, Property (i) states that we can relax correct constraints without violating their correctness. The reverse does not hold, otherwise, the inconsistent constraint $\bot$ would describe every system. The formalization of relaxation of constraints as described by Property (i) allows us to generalize constraints and therefore plays a crucial role in modeling abstraction.

Property (ii) requires that for any set of constraints $\mathbf{L^{\prime}}$ there exist a “best” constraint that correctly describes any system described by every constraint in $\mathbf{L^{\prime}}$. We can apply this property to the constraints derived from several models to narrow down our description of a given system’s properties. In this sense, it allows us to derive a specific result from a number of more general results. Note that the converse of (ii) follows from (i), so (ii) could also be written as a biconditional.

III-D Abstraction and Concretization

Given a correctness relation $R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}$ for $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$, we desire to define a mapping between $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ and a modeling formalism $\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}$ that induces a correctness relation $R_{\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}}:\mathcal{S}\rightarrow\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}$. Furthermore, this mapping must allow for the modeling domain to abstract system constraints. For instance, a topology model should be able to discard constraints on component reliability.

The formalism of choice for this task is a Galois connection:

Definition III.2

A Galois Connection $(\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}},\alpha,\gamma,\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}})$ between two complete lattices $\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}$ and $\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}$ consists of a pair of monotone functions $\alpha:\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}\rightarrow\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}$ and $\gamma:\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}\rightarrow\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}$ for which the following relationships hold:

[TABLE]

We refer to $\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}$ as the concrete domain, $\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}$ as the abstract domain, $\alpha$ as the abstraction operator, and $\gamma$ as the concretization operator.

In terms of models and properties, $\alpha$ abstracts a model, $m$, from a set of constraints on a system, $p$, and $\gamma$ derives, or concretizes, system constraints from a model of that system. Relationship (1) states that abstracting the model $m$ from constraints $p$, then concretizing constraints from that model, results in constraints that are at most more general than those of $p$. In other words, abstraction may relax constraints irrelevant to the model formalism, but it cannot produce a model that implies constraints that contradict $p$. Relationship (2) requires that $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ be able to completely capture the constraints imposed by each model formalism, meaning that if constraints are concretized from a model, $m$, of a system, any other model abstracted from these constraints will be as least as specific as the original model, $m$. Concretization may introduce additional constraints, but in practice, the $\sqsubseteq$ of (2) will often be strict equality in practice.

Next, we show that each Galois connection induces a correctness relation $R_{\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}}$ on the abstract domain.

Theorem III.1

Given a Galois connection $(\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}},\alpha,\gamma,\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}})$ and a correctness relation $R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}:\mathcal{S}\rightarrow\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}$, the relation $R_{\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}}:\mathcal{S}\rightarrow\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}$ defined by $s\,R_{\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}}\,m\iff s\,R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}\,\gamma(m)$ is a correctness relation.

Proof:

We must show that properties (i) and (ii) from Definition III.1 hold for $R_{\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}}$. Take $s\in\mathcal{S}$ and $m_{1},m_{2}\in\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}$.

[TABLE]

The proof of (ii) uses the fact that $\gamma$ is completely multiplicative, that is, \mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\{\gamma(m)\mid m\in\mathbf{M^{\prime}}\}=\gamma\left(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{M^{\prime}}\right). Take $s\in\mathcal{S}$ and $\mathbf{M^{\prime}}\subseteq\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}$.

[TABLE]

∎

Put in terms of models and system properties, if we define a Galois connection between $\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ and the lattice for a given modeling formalism $\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}$, then every correct collection of system constraints abstracts to a correct model and every correct model concretizes to a correct collection of system constraints. Therefore, we have developed a provably sound definition of the nature of model abstraction.

III-E Model Transformation

Given this formalization of system and model semantics, we can now formalize the problem of model transformation. Suppose we have a properties domain and two modeling formalisms with associated Galois connections to the properties domain $(\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}},\alpha_{\mathbb{\StrLeft{M_{1}}{1}}\mathbf{\StrGobbleLeft{M_{1}}{1}}},\gamma_{\mathbb{\StrLeft{M_{1}}{1}}\mathbf{\StrGobbleLeft{M_{1}}{1}}},\mathbb{\StrLeft{Model_{1}}{1}}\mathbf{\StrGobbleLeft{Model_{1}}{1}}$) and $(\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}},\alpha_{\mathbb{\StrLeft{M_{2}}{1}}\mathbf{\StrGobbleLeft{M_{2}}{1}}},\gamma_{\mathbb{\StrLeft{M_{2}}{1}}\mathbf{\StrGobbleLeft{M_{2}}{1}}},\mathbb{\StrLeft{Model_{2}}{1}}\mathbf{\StrGobbleLeft{Model_{2}}{1}}$). Furthermore, we have a correctness relation $R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}$ which induces correctness relations $R_{\mathbb{\StrLeft{M_{1}}{1}}\mathbf{\StrGobbleLeft{M_{1}}{1}}}$ and $R_{\mathbb{\StrLeft{M_{2}}{1}}\mathbf{\StrGobbleLeft{M_{2}}{1}}}$.

Definition III.3

A model transformation from $\mathbb{\StrLeft{Model_{1}}{1}}\mathbf{\StrGobbleLeft{Model_{1}}{1}}$ to $\mathbb{\StrLeft{Model_{2}}{1}}\mathbf{\StrGobbleLeft{Model_{2}}{1}}$ is a semantically sound mapping $\tau_{\mkern 2.0mu\mathbb{\StrLeft{M_{1}}{1}}\mathbf{\StrGobbleLeft{M_{1}}{1}}}^{\mathbb{\StrLeft{M_{2}}{1}}\mathbf{\StrGobbleLeft{M_{2}}{1}}}:\mathbb{\StrLeft{Model_{1}}{1}}\mathbf{\StrGobbleLeft{Model_{1}}{1}}\rightarrow\mathbb{\StrLeft{Model_{2}}{1}}\mathbf{\StrGobbleLeft{Model_{2}}{1}}$. That is, if $m_{1}\in\mathbb{\StrLeft{Model_{1}}{1}}\mathbf{\StrGobbleLeft{Model_{1}}{1}}$ is correct, then $\tau_{\mkern 2.0mu\mathbb{\StrLeft{M_{1}}{1}}\mathbf{\StrGobbleLeft{M_{1}}{1}}}^{\mathbb{\StrLeft{M_{2}}{1}}\mathbf{\StrGobbleLeft{M_{2}}{1}}}(m_{1})$ is also correct.

We can define $\tau_{\mkern 2.0mu\mathbb{\StrLeft{M_{1}}{1}}\mathbf{\StrGobbleLeft{M_{1}}{1}}}^{\mathbb{\StrLeft{M_{2}}{1}}\mathbf{\StrGobbleLeft{M_{2}}{1}}}$ by first concretizing constraints from $m_{1}\in\mathbb{\StrLeft{Model_{1}}{1}}\mathbf{\StrGobbleLeft{Model_{1}}{1}}$, then abstracting an element of $\mathbb{\StrLeft{Model_{2}}{1}}\mathbf{\StrGobbleLeft{Model_{2}}{1}}$ from it.

Theorem III.2

The mapping $\tau_{\mkern 2.0mu\mathbb{\StrLeft{M_{1}}{1}}\mathbf{\StrGobbleLeft{M_{1}}{1}}}^{\mathbb{\StrLeft{M_{2}}{1}}\mathbf{\StrGobbleLeft{M_{2}}{1}}}(m_{1})=(\alpha_{\mathbb{\StrLeft{M_{2}}{1}}\mathbf{\StrGobbleLeft{M_{2}}{1}}}\circ\gamma_{\mathbb{\StrLeft{M_{1}}{1}}\mathbf{\StrGobbleLeft{M_{1}}{1}}})(m_{1})$ is sound.

Proof:

Take $s\in\mathcal{S}$ and $m_{1}\in\mathbb{\StrLeft{Model_{1}}{1}}\mathbf{\StrGobbleLeft{Model_{1}}{1}}$.

[TABLE]

∎

To sum up the transformation process: begin with a model $m_{1}\in\mathbf{Model_{1}}$. Concretize properties of the system from $\{m_{1}\}$, then apply $\tau_{\mkern 2.0mu\mathbb{\StrLeft{M_{1}}{1}}\mathbf{\StrGobbleLeft{M_{1}}{1}}}^{\mathbb{\StrLeft{M_{2}}{1}}\mathbf{\StrGobbleLeft{M_{2}}{1}}}$ to produce a set of models $M^{\prime}_{2}\subseteq\mathbf{Model_{2}}$. Finally, select a model from $M^{\prime}_{2}$ by introducing information about the system not present in $m_{1}$.

Figure 1 illustrates the domains, mappings, and relationships present in this formalization of model transformation.

III-F Selection and Specificity

Recall that the elements of $\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}$ are sets of models. To concretize properties of a single model $m\in\mathbf{Model}$, we first map it to $\{m\}\in\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}$, then apply $\gamma$. Conversely, for a set of models $M$ produced from an abstraction operation, each model in that set equally captures the system constraints from which $M$ was abstracted. If $M=\emptyset$, then the chosen modeling formalism cannot reason about the given system constraints. If $M=\{m\}$, then the abstraction process has produced a single model describing the system. Otherwise, the system constraints lack some information about the system that is relevant to this modeling formalism. In this case, the user must introduce new information about the system by selecting one model from this set. For example, one may have to provide information about component reliability when selecting a reliability model.

We represent this selection process as a function $\sigma:\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}\rightarrow\mathbf{Model}$; the definition of $\sigma$ depends entirely upon the exact system being modeled. While the known system constraints may not be precise enough to indicate exactly which model in the set is correct, they still indicate that the correct model is in the given set of models. Therefore we can constrain $\sigma$ to not produce a model which we know is incorrect even when we do not have enough information about the system to produce a single model.

Definition III.4

The function $\sigma:\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}\rightarrow\mathbf{Model}$ is a selection operator if the following conditions hold:

1. (i)

$\sigma(m)\in m$** 2. (ii)

If $s\,R_{\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}}\,m$, then $s\,R_{\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}}\,\{\sigma(m)\}$

Given a selection operator, we can incorporate the newly introduced information back into the system properties domain, allowing future transformations to include these constraints and therefore produce more specific results. Take $p\in\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ such that $s\,R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}\,p$. Derive the exact model of formalism $\mathbb{\StrLeft{Model}{1}}\mathbf{\StrGobbleLeft{Model}{1}}$ by letting $m:=(\sigma\circ\alpha)(p)$. By definition of $\sigma$ we know $s\,R_{\mathbb{\StrLeft{M}{1}}\mathbf{\StrGobbleLeft{M}{1}}}\,\{m\}$, so $s\,R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}\,\gamma(\{m\})$. Finally, we can construct a more specific element $p^{\prime}\in\mathbb{\StrLeft{Properties}{1}}\mathbf{\StrGobbleLeft{Properties}{1}}$ by $p^{\prime}:=p\sqcap\gamma(\{m\})$. The correctness of $p^{\prime}$ follows from property (ii) for $R_{\mathbb{\StrLeft{P}{1}}\mathbf{\StrGobbleLeft{P}{1}}}$, and by definition of $\sqcap$, $p^{\prime}\sqsubseteq p$.

Figure 2 depicts the relationship between these given functions and domains.

IV Tag-Options Lattice

In our formalization of systems and models, we assume a properties domain that is a lattice of constraints on a system; its elements are ordered by specificity. A common pattern arises when defining this domain: a lattice that assigns a set of potential values to each element of a set of names or tags. Two examples are assigning possible reliabilities to components and defining whether a state is considered functional or failed. We will refer to this type of lattice as a Tag–Options Lattice; it is comprised of a tag lattice and a family of options lattices. For instance, one may use a tag lattice where each element is a set of components known to be part of a system; each element of the corresponding options lattice is a function that assigns possible reliabilities to each component.

IV-A Tag Lattice

Let $\mathbf{T}:=\{t_{1},t_{2},\cdots\}$ be a set of tags.

Definition IV.1

The tag lattice $\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}:=\mathcal{P}(\mathbf{T})^{\partial}$ is the dual of the powerset lattice of $\mathbf{T}$, where $\sqsubseteq:=\supseteq$, \mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}:=\bigcup, and $\bigsqcup:=\bigcap$.

In this lattice, $\top=\emptyset$ corresponds to a system where no tags are known to apply—for example, a system with no known components. Thus, every system is described by $\top$. Lattice elements are ordered by specificity; if $T_{1},T_{2}\in\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}$ and $T_{1}\sqsubseteq T_{2}$, then $T_{1}$ contains more information than $T_{2}$ about tags that apply to a system.

IV-B Options Lattice Family

Let $\mathbf{O}=\{o_{1},o_{2},\cdots\}$ denote the set of options—potential values—for each tag.

Definition IV.2

For each set of tags $\mathbf{T^{\prime}}\in\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}$ we can define a corresponding options lattice $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}$. The elements of $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}$ are functions $f:\mathbf{T^{\prime}}\rightarrow\mathcal{P}(\mathbf{O})$ that assign a set of possible options to each tag. For any $f,g\in\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}$, $f\sqsubseteq g$ if and only if $f(t)\subseteq g(t)$ for all $t\in\mathbf{T^{\prime}}$.

We can alternatively view the elements as sets of tuples $(t,\mathbf{o})$ where $t\in\mathbf{T^{\prime}}$ and $\mathbf{o}\in\mathcal{P}(\mathbf{O})$. Each set contains exactly one tuple per tag.

For any set of elements of an options lattice, $\mathbf{O^{\prime}}\subseteq\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}$, we define

1. i)

$\bigsqcup\mathbf{O^{\prime}}=\lambda t.\bigcup\{f(t)\mid f\in\mathbf{O^{\prime}}\}$, and 2. ii)

\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{O^{\prime}}=\lambda t.\bigcap\{f(t)\mid f\in\mathbf{O^{\prime}}\}.

We refer to the family of options lattices associated with tag set $\mathbf{T}$ by $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T})$.

For example, if $\mathbf{T^{\prime}}:=\{t_{1},t_{2}\}$ and $\mathbf{O}:=\{x,y\}$, then $f:=\{(t_{1},\emptyset),(t_{2},\{x,y\})\}$ and $g:=\{(t_{1},\{x\}),(t_{2},\{y\})\}$ are elements of $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}$. Furthermore,

[TABLE]

Theorem IV.1

$\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}$* is a complete lattice.*

Proof:

The proof that $\sqsubseteq$ is a partial order on $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}$ follows directly from $\subseteq$ being a partial order on $f(t),f\in\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}$ for all $t\in\mathbf{T^{\prime}}$. Likewise, the proof that \mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}} and $\bigsqcup$ are complete follows from the completeness $\bigcap$ and $\bigcup$. ∎

From these definitions it follows that $\top(t)=\mathbf{O}$ and $\bot(t)=\emptyset$ for all $t\in\mathbf{T^{\prime}}$. We can always imagine a system where any of the given options holds for each tag; a system where no tag corresponds to any of the options is a system about which our abstractions cannot reason.

Hasse diagrams for $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\{t_{1}\}}$ and $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\{t_{1},t_{2}\}}$ are shown in Figure 3 and Figure 4, respectively.

Thus far, we have defined a lattice of system tags $\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}$ and a family of options lattices $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T}):=\{\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}\mid\mathbf{T^{\prime}}\in\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}\}$ consisting of mappings of tags to options. What remains is to combine these lattices into a single tag–options lattice.

IV-C Options Lattice Homomorphisms

Before we can develop a tag–options lattice, we must define how elements of different options lattices are related. The tool of choice is a lattice homomorphism: a mapping between lattices that preserves meets and joins.

Definition IV.3

For all sets of tags $\mathbf{A},\mathbf{B}\in\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}$ we define a function $\phi_{A}^{B}:\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{A}}\rightarrow\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{B}}$ by

[TABLE]

Or, from a sets-of-tuples perspective,

[TABLE]

$\phi$ allows us to convert a function with one domain to a related function with a different domain: if $f:\mathbf{A}\rightarrow\mathcal{P}(\mathbf{O})$, then $\phi_{A}^{B}(f):\mathbf{B}\rightarrow\mathcal{P}(\mathbf{O})$.

Theorem IV.2

$\phi_{A}^{B}$* is a lattice homomorphism. That is, for all $\mathbf{O^{\prime}}\subseteq\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{A}}$,*

1. i)

\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\left\{\phi_{A}^{B}(f)\mid f\in\mathbf{O^{\prime}}\right\}=\phi_{A}^{B}\left(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{O^{\prime}}\right)* and* 2. ii)

$\bigsqcup\left\{\phi_{A}^{B}(f)\mid f\in\mathbf{O^{\prime}}\right\}=\phi_{A}^{B}\left(\bigsqcup\mathbf{O^{\prime}}\right)$.

Proof:

To show \mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\left\{\phi_{A}^{B}(f)\mid f\in\mathbf{O^{\prime}}\right\}=\phi_{A}^{B}\left(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{O^{\prime}}\right), suppose $\mathbf{A},\mathbf{B}\subseteq\mathbf{T}$ and $\mathbf{O^{\prime}}\subseteq\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{A}}$ and take arbitrary $t\in\mathbf{B}$.

Case 1: $t\in\mathbf{A}$.

[TABLE]

Case 2: $t\notin\mathbf{A}$.

[TABLE]

The proof that $\bigsqcup\left\{\phi_{A}^{B}(f)\mid f\in\mathbf{O^{\prime}}\right\}=\phi_{A}^{B}\left(\bigsqcup\mathbf{O^{\prime}}\right)$ is analogous. ∎

We now prove a corollary necessary to show the completeness of the tag–option lattice:

Theorem IV.3

If $\mathbf{A},\mathbf{B},\mathbf{C}\in\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}$ such that $\mathbf{A}\sqsubseteq\mathbf{B}\sqsubseteq\mathbf{C}$ and $f\in\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{A}}$ and $g\in\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{C}}$ such that $\phi_{A}^{C}(f)\sqsubseteq g$, then $\phi_{A}^{B}(f)\sqsubseteq\phi_{C}^{B}(g)$.

Proof:

Take arbitrary $t\in\mathbf{B}$.

Case 1: $t\in\mathbf{C}$. Then $f(t)\subseteq g(t)$, $\phi_{A}^{B}(f)(t)=f(t)$, and $\phi_{C}^{B}(g)(t)=g(t)$. Therefore $\phi_{A}^{B}(f)(t)\subseteq\phi_{C}^{B}(f)(t)$.

Case 2: $t\not\in\mathbf{C}$. Then $\phi_{C}^{B}(g)(t)=\mathbf{O}$ and $\phi_{A}^{B}(f)(t)\subseteq\mathbf{O}$. ∎

IV-D Tag-Options Lattice

So far, we have developed a lattice that relates sets of tags that apply to a given system and a family of lattices that relate option values given a set of tags. Now we combine these into a lattice that can relate option values between sets of tags.

Definition IV.4

A tag–options lattice $\mathbbg{\Lambda}(\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}},\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T}))$ is a lattice of tuples $(\mathbf{T^{\prime}},f)$ where $\mathbf{T^{\prime}}$ is an element of $\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}$ and $f$ is an element of $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T^{\prime}}}$. Given elements $(\mathbf{A},f)$ and $(\mathbf{B},g)\in\mathbbg{\Lambda}(\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}},\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T}))$, $(\mathbf{A},f)\sqsubseteq(\mathbf{B},g)$ if and only if $\mathbf{A}\sqsubseteq\mathbf{B}$ and $\phi_{A}^{B}(f)\sqsubseteq g$.

(Note that if $(\mathbf{A},f)\sqsubseteq(\mathbf{B},g)$, $\mathbf{A}\sqcup\mathbf{B}=\mathbf{B}$, so $\phi_{A}^{A\sqcup B}=\phi_{A}^{B}$ and $\phi_{B}^{A\sqcup B}=\lambda x.x$.)

For any subset $\mathbf{\Lambda}\subseteq\mathbbg{\Lambda}(\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}},\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T}))$, let $\mathbf{V}:=\{T^{\prime}\mid(T^{\prime},f)\in\mathbf{\Lambda}\}$. Then we can define

1. i)

$\bigsqcup\mathbf{\Lambda}:=\left(\bigsqcup\mathbf{V},\bigsqcup\left\{\phi_{T^{\prime}}^{\bigsqcup\mathbf{V}}(f)\mid(T^{\prime},f)\in\mathbf{\Lambda}\right\}\right)$, and 2. ii)

\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{\Lambda}:=\left(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{V},\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\left\{\phi_{T^{\prime}}^{\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{V}}(f)\mid(T^{\prime},f)\in\mathbf{\Lambda}\right\}\right).

In this lattice, $\bot=(\bot_{\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}},\bot_{\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T}}})$ is the system where no options are valid for any tag. $\top=(\top_{\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}},\top_{\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{\emptyset}}})$ corresponds to the system where no tags are known to apply.

For example, suppose we have a set of tags $\mathbf{T}=\{t_{1},t_{2},t_{3}\}$ and take elements $\mathbf{T_{1}},\mathbf{T_{2}}\in\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}$ where $\mathbf{T_{1}}=\{t_{1},t_{2}\}$, and $\mathbf{T_{2}}=\{t_{2},t_{3}\}$. Let the options set be $\mathbf{O}=\{x,y\}$.

Let $f:\mathbf{T_{1}}\rightarrow\mathcal{P}(\mathbf{O})$ be an element of $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T_{1}}}$ where $f=\{(t_{1},\emptyset),(t_{2},\mathbf{O})\}$. Let $g:\mathbf{T_{2}}\rightarrow\mathcal{P}(\mathbf{O})$ be an element of $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}_{\mathbf{T_{2}}}$ where $g=\{(t_{2},\{x\}),(t_{3},\{y\})\}$. Then $(T_{1},f)$ and $(T_{2},g)$ are elements of $\mathbbg{\Lambda}(\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}},\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T}))$.

Furthermore, we can compute the meet of $(T_{1},f)$ and $(T_{2},g)$ as follows:

[TABLE]

Theorem IV.4

$\mathbbg{\Lambda}(\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}},\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T}))$* is a complete lattice.*

Proof:

That $\sqsubseteq$ is a partial order follows from the partial orders defined on $\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}}$ and the lattices of $\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T})$.

To show that \mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}} is a well–defined meet operator, take an arbitrary subset $\mathbf{\Lambda}\subseteq\mathbbg{\Lambda}(\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}},\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T}))$, and let $\mathbf{V}:=\{T\mid(T,f)\in\mathbf{\Lambda}\}$.

Take arbitrary $(T^{\prime},f^{\prime})\in\mathbbg{\Lambda}(\mathbb{\StrLeft{T}{1}}\mathbf{\StrGobbleLeft{T}{1}},\mathbb{\StrLeft{O}{1}}\mathbf{\StrGobbleLeft{O}{1}}(\mathbf{T}))$ such that $\forall l\in\mathbf{\Lambda},(T^{\prime},f^{\prime})\sqsubseteq l$. Thus, T^{\prime}\sqsubseteq\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{V}. Furthermore,

[TABLE]

Therefore (T^{\prime},f^{\prime})\sqsubseteq\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{\displaystyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\textstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptstyle\bigsqcup}}{\rotatebox[origin={c}]{180.0}{\scriptscriptstyle\bigsqcup}}}\mathbf{\Lambda}. The proof that $\bigsqcup$ is a well–defined join operator is analogous. ∎

For an example of how a tag–options lattice might be used to construct a concrete properties domain, consider the task of assigning reliabilities to components. In this case, we define a set of component names $\mathbf{Components}:=\{c_{1},c_{2},\cdots\}$ to use as tags. The elements of the tag lattice $\mathbb{\StrLeft{Components}{1}}\mathbf{\StrGobbleLeft{Components}{1}}:=\mathcal{P}(\mathbf{Components})^{\partial}$ consist of sets of component names. If an element of $\mathbb{\StrLeft{Components}{1}}\mathbf{\StrGobbleLeft{Components}{1}}$ applies to a given system, then we know that the system consists of at least those components. The set of options is $\mathbf{Probability}=\{x\in\mathbb{R}\mid 0<x\leq 1\}$. Finally, the tag–options lattice $\mathbbg{\Lambda}(\mathbb{\StrLeft{Components}{1}}\mathbf{\StrGobbleLeft{Components}{1}},\mathbb{\StrLeft{Probability}{1}}\mathbf{\StrGobbleLeft{Probability}{1}}(\mathbf{Components}))$ consists of pairs $(\mathbf{C},p)$ where $\mathbf{C}$ is a set of components known to comprise a given system and $p(c)$ assigns a range of possible reliabilities to each $c\in\mathbf{C}$. Thus $\mathbbg{\Lambda}(\mathbb{\StrLeft{Components}{1}}\mathbf{\StrGobbleLeft{Components}{1}},\mathbb{\StrLeft{Probability}{1}}\mathbf{\StrGobbleLeft{Probability}{1}}(\mathbf{Components}))$ is a lattice of constraints on component reliability ordered by specificity. It can be used as part of a definition of a properties domain in conjunction with other lattices that capture other relevant system properties.

V Conclusion and Future Work

In this paper, we have demonstrated a formalization of model and system semantics. Models abstract system semantics; therefore, we can derive, or concretize, constraints on a system from models of it. Conversely, given constraints on a system, we can abstract a set of models that are consistent with those constraints.

To formalize the soundness of this approach, we apply abstract interpretation, which defines a correctness relation between systems and constraints. If our abstraction and concretization mappings between a given modeling formalism and system constraints form a Galois connection between the two domains, we can show that these mappings and the correctness relation for system constraints induce a correctness relation between systems and the models of the modeling formalism.

Through this lens, the process of model transformation becomes the process of concretizing system properties from one model, then abstracting a second model from these properties. We show that this process is sound; that is, if the initial model is correct, then the final model will also be correct.

Future work will take several directions. We are currently working on relating models of different aspects of a system—in this case, reliability and topology. This work will demonstrate both how topology affects system reliability by introducing dependencies between components and how reliability, via the same dependencies and the constraints on system functionality, constrains the choice of topologies for which that definition of reliability holds.

We plan to further extend the work of this paper to other model types and other choices of system properties. Expanding the possible transformations will allow us to relate modeling techniques from various system domains; for example, we may apply a water distribution network analysis technique to a power grid, or incorporate both cyber and physical models into a cyber–physical model.

Another avenue of research is to expand the formalization of models and systems to other metamodeling tasks. A salient challenge in the design of complex systems is that of heterogeneous model composition: combining component models that use various modeling formalisms into a single model of a complete system. The abstraction and concretization functions defined in this work provide a basis for developing these connections. It may even be possible to perform this composition at a higher level, enabling the creation of hybrid modeling formalisms and associated solution and evaluation techniques.

Finally, the task of developing this approach into a tool for system designers will certainly present its own challenge. Such a tool must be interactive and scalable to complex, real–world systems, all without requiring the user to have a deep understanding of the underlying theory.