Theme 2: Methodologies, Models, and Tools
Note that this theme was renumbered in the fall of 2015. Formerly, it was Theme 4.
A key challenge in designing TerraSwarm applications and infrastructure is that the distinction between "design time" and "run time" becomes blurred. Ensuring that different components and subsystems can be dynamically recombined yet still function properly will require new, highly advanced development methodologies, models, and tools. Functions to be realized must be separated from the components that will be used to realize them (the "separation of concerns" concept (see ). Programming models must be less centered on algorithms (step-by-step transformation of data) and more centered on dynamics (change of state over time), distribution, discovery, and adaptation. Optimizations that might be performed at design time in a conventional system-of-systems, such as mapping of functions to resources, will need to be performed at run time. Design-time testing and verification will not be adequate, because components and applications are dynamically composed and recomposed. Validation will need to be performed at a higher level, will need to cover families of possible run-time configurations rather than just one, and will need to include run-time validation strategies that are lightweight and energy efficient.
The goal of this theme is to develop methodologies, models, and tools that support the unique requirements of TerraSwarm systems. Critical research areas include advanced modeling, verification, and adaptation approaches, described further below. This theme is intertwined with the others and provides the theory and tools support to the entire TerraSwarm effort.
Modeling. Developing TerraSwarm systems will require the ability to effectively model system components and their interactions. Models must capture the evolving availability of services and resources, which can potentially be combined to provide many different types of applications. Models must also capture the rules for recruiting and combining resources and services. Current modeling approaches do not support the complex, dynamically changing characteristics of TerraSwarm systems.
We will model TerraSwarm systems as a dynamic hierarchical graph of components that comprise the system. The nodes of the graph will represent services. Since these graphs are hierarchical, a node may itself be a graph aggregating sub-services to define a new service. The edges in the graph represent (i) communication paths between components; (ii) authority relations between components; (iii) use relationships (i.e., service x uses service y); (iv) ownership relations; (v) coordination; (vi) controllability; and (vii) observability.
A TerraSwarm system's behavior is the result of run-time and design-time optimization processes that choose the configuration that will best achieve its goals. A conguration of a TerraSwarm system is a particular graph structure that selects specific capabilities of the nodes in the graph (i.e., subsystems).
Verification. Verification of TerraSwarm systems' functionality will be difficult. The large number of components, their heterogeneity, and the dynamically changing structure will render exhaustive formal verification impractical. Instead, we will need compositional and incremental techniques. Compositional techniques hierarchically infer properties of compositions from properties of components. Incremental techniques infer properties of a configuration from properties of a similar configuratio.
Compositional verification is enabled by assume-guarantee reasoning, which requires models of the environment. (Assume-guarantee contracts are described in .) In a dynamic TerraSwarm context, these models will likely be incomplete, and hence will need to be inferred or refined from observations. Such models will be imperfect, and therefore should include metrics of uncertainty that verification techniques can reason about.
In the dynamic network of a TerraSwarm system, non-interference properties will become key. For example, when a node joins or leaves a network, it must not disrupt any service that does not depend on this node. Non-interference of temporal properties becomes particularly important for closed-loop cyber-physical systems, because if one service disrupts the timing of another, it may change the dynamics of a physical system in undesirable ways. Hence, models will need to include temporal specifications that verification techniques can reason about.
Finally, not all nodes will be equally trusted. TerraSwarm protocols will need to detect compromises, distinguished trusted from untrusted data and resources, and be robust to the presence of a certain number of malicious nodes. Techniques based on a combination of formal methods and algorithmic game theory can be effective in analyzing the impact of malicious agents. Tools for formal verification of composition and abstraction-refinement relations using horizontal and vertical contracts will be developed together with other verification techniques based on functional and architectural simulation. Indeed, contracts are critical in defining and verifying compositionality and the abstraction-refinement relation among the different layers of abstraction of a TerraSwarm system.
Adaptation. TerraSwarm applications will need to deploy resources dynamically in order to achieve mission goals, and these goals may change based on circumstances encountered in the field. Typical optimization strategies for determining how best to deploy resources depend on knowing the spatial probability distribution of relevant events - but in a TerraSwarm system, this distribution will not be known in advance.
By leveraging theoretical and algorithmic tools developed for adaptive systems, we can derive new simple algorithms for complex tasks, such as coverage, source seeking, distributed partitioning, and tracking under uncertain communication constraints. These algorithms do not depend on a model of the environment, exploiting instead event observations during deployment. Moreover, they adapt to slowly varying environmental conditions or sudden but infrequent environmental changes.
Methodologies, Models, and Tools
- Alberto Sangiovanni-Vincentelli (Leader)
- Sanjit A. Seshia (Co-Leader)
- See the Tools Overview for a list of other faculty.
You are not logged in or do not have access to most of this workgroup. Admins, to edit this page, see the profile.