Synthesis of Correct-By-Construction Control Protocols for Open, Reconfigurable
The realization of autonomy in networks on naval platforms---beyond today’s norm of stand-alone unmanned vehicles---calls for new protocol-based controllers that blend continuous decisions with discrete, logic-based, network-wide decisions. They will be enabled by advanced perception, software with multiple threads and communication over constrained media. Furthermore, they are expected to support the emerging trends toward integrated functionality and open, modular architectures for design- and run-time affordability.
Despite numerous complicating factors, the design-verification cycle for open, networked systems is often ad hoc mainly due to our lack of appropriate algorithms and computational tool support. We focus on this very bottleneck by shifting from the conventional "first design, then try to verify" approach to a "formally specify and automatically synthesize" procedure. This fresh perspective will diffuse the intent of establishing trust throughout the design flow, suppress the complexity, and facilitate post-design upgrades.
We partition the proposed effort into three research thrusts and a cross-cutting validation plan:
- Formal specifications and automated synthesis: We will develop synthesis algorithms that can handle complex dynamics with discrete topology changes under stochasticity and limited network-wide awareness subject to temporal logic specifications.
- Integration of functionalities and virtualization of services: We will develop algorithms that leverage the multitude of sense-compute-actuate capabilities and communication to dynamically allocate resources and improve efficiency and resilience through integration of functionality.
- Modular and incremental synthesis: We will investigate how a priori architectural constraints, e.g., modularity, can be introduced into protocol synthesis to enhance scalability, allow addition/removal of components in a plug-and-play manner and incrementally evolve verified controllers from one generation to the next without a re-design from scratch.