Visible to the public CPS: Breakthrough: Compositional Modeling of Cyber-Physical Systems Conflict Detection Enabled

Project Details
Lead PI:Rance Cleaveland
Performance Period:09/01/15 - 08/31/17
Institution(s):University of Maryland College Park
Sponsor(s):National Science Foundation
Award Number:1446665
948 Reads. Placed 221 out of 803 NSF CPS Projects based on total reads on all related artifacts.
Abstract: Title: CPS: Breakthrough: Compositional Modeling of Cyberphysical Systems This project is devoted to the discovery of new mathematical modeling techniques for Cyber-Physical Systems. In particular, the research involves devising novel conceptual methods for assembling systems from subsystems, and for reasoning about the behavior of systems in terms of the behavior of their subsystems, which may be computational or physical. The results enable scientists and engineers to develop more realistic models of the systems they are designing, and to obtain greater insights into their eventual behavior, without having to build costly prototypes. The intellectual merits are the new notions of system behavior being developed that unify the computational and the physical, and the mathematical operators and laws governing the relationships between systems and subsystems. The project's broader significance and importance lie in the increased pace of innovation within Cyber-Physical System design that the new modeling techniques make possible, and the curricular enhancements that the novel conceptual frameworks under development support. The specific research program of this project involves the development of a novel modeling paradigm, Generalized Synchronization Trees (GSTs), into a rich framework for both describing Cyber-Physical Systems (CPSs) and studying their behavior under interconnection. GSTs are inspired by Milner's use of Synchronization Trees (STs) to model interconnected computing processes, but GSTs generalize the mathematical structure of their forebears in such a way as to encompass systems with discrete ("Cyber") as well as continuous ("Physical") dynamics. As Milner did with STs, the PIs are developing an algebraic theory of composition for GSTs. Such theories have a particular advantage over non-algebraic ones: because the composition of two (or more) objects results in an object of the same type, composition operators can be nested to build large structures out of smaller ones. Thus, the theory of GSTs is inherently compositional. The development of the theory involves five distinct but complementary endeavors. Standard models for cyber-physical systems are being encoded as GSTs in a semantically robust way; meaningful notions of composition and congruence for CPSs are being described and studied algebraically; the interplay between behavioral equivalence and the preservation of system properties is being investigated; a notion of real-time (or clock time) is under consideration for GSTs; and GSTs are being assessed as modeling tools for practical design scenarios.