A co-synthesis approach based on symbolic reachability analysis

In this paper we present a co-synthesis approach based on the state space reachability analysis of the system specification, which is captured using a partial order based model for concurrency. The partial order based model (POM) combines the concept of relations between events from event structures for the modeling of intercommunicating concurrent behaviors and the Chu space semantics for these relations in terms of logical formulas. The POM is used in our approach as an intermediate representation, which permits a concise symbolic representation, mainly for systems with high degree of parallelism, and an efficient BDD based implementation of analysis and synthesis algorithms. We introduce the partial order based model for concurrency and show how to use it in modeling at the system level. We present a symbolic representation for the model and its implementation using BDDs and we give reachability analysis algorithms that are applied to the estimation of performance and costs during the co-synthesis and to the formal verification of properties. Finally we describe our co-synthesis approach based on the formal model