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.