Compositional Cyber-Physical Systems Theory

A major impedance to engineering safe and secure cyber-physical systems is the lack of formal relationships between different types of models necessary for design. These various models are necessary because of the coupled physical and computational dynamics present in cyber-physical systems as well as the different properties system designers want to assure about a system. Each of the individual models has a set of rules describing what operations are allowed and which are not, including how to compose elements together in a way that is correct. These can mathematically be seen as algebras. However, the algebras in the engineering of correct and complete requirements, the specification and validation of dynamical behavior, and the identification of software and hardware architectures to carry out the necessary functions are distinct and can potentially lead to designing-in hazardous behavior in safety critical cyber-physical systems.

This dissertation builds a compositional cyber-physical systems theory to develop concrete semantics relating the above diverse views necessary for safety and security assurance. In this sense, composition can take two forms. The first is composing larger models from smaller ones within each individual formalism of requirements, behaviors, and architectures which can be thought of as horizontal composition—a problem which is largely solved. The second and main contribution of this theory is vertical composition, meaning relating or otherwise providing verified composition across requirement, behavioral, and architecture models and their associated algebras. In this dissertation, we show that one possible solution to vertical composition is to use tools from category theory. Category theory is a natural candidate for making both horizontal and vertical composition formally explicit because it can relate, compare, and/or unify different algebras.

Ultimately, category theory reframes the problem of abstraction, either in the management of mathematical structures or system models by positioning a problem in its most natural domain. Category theory does not model the internal structure of the objects it acts upon. Instead, a categorical formalism perceives an object through its relationships with other objects and not by what the object is individually. Indeed, in this context we focus on abstraction, which we see as determining only what is essential in each layer of a given model. This allows us to talk about how things are related instead of focusing on how things are. This mindset as applied to systems theory gives rise to a circumspection of the system where we do not examine a system by its individual elements but by looking at the compositional structure of the system, which includes both the individual constituents and their interconnections. This is all to say that through compositional cyber-physical systems theory we can give concrete meaning to abstraction and refinement in cyber-physical system models, which can assist with the specification (and eventual validation) of increasingly complex systems.

Using this relational understanding of modeling we formalize categorically behavior and architecture using the systems as algebras framework, where boxes are subsystems and wires are connections between subsystems. This is a two step process. First we define the interface of each box as well as the way in which the boxes ought to be interconnected to compose the total system. Second, we assume a behavioral formalism for each box that is congruent with the behavior of other boxes based on the way they are interfaced and connected. We apply this framework to safety through the means of contracts and to security through the means of tests and actions. Finally, we show how these different algebras and categorical structures can be used to mathematically implement verified composition.