Synthesizing embedded software with safety wrappers through polyhedral analysis in a polychronous framework

摘要

Polychrony, a model of computation, allows us to statically analyze safety properties from formal specifications and synthesize deterministic software for safety-critical cyber physical systems. Currently, the analysis is performed on the formal specifications through Boolean abstractions. Even though it is a sound abstraction, for more precise analysis we might have to refine the abstraction. Refining the abstraction level from pure Boolean to a theory of Integers can lead to more precise decisions. In this paper, we first show how integrating a Satisfiability Modulo Theory (SMT) solver to POLYCHRONY compiler can enhance its decision making capabilities. Further, we show, how a polyhedral analysis library integrated to the compiler, can compute safe operational boundaries, and filter unsafe input combinations to keep the system safe. We enhanced the POLYCHRONY compiler's ability to make more accurate decisions and to accept and characterize the safe input range for specifications where safety may be violated for a relatively small region of a large input space. The enhancement also allows the user to consider the severity of the violation with respect to entire space of inputs, and either reject a specification or synthesize a wrapped software with guaranteed safe operation.