Compositional synthesis of concurrent systems through causal model checking and learning

Abstract

Formal verification such as model checking can be used to verify whether a system model satisfies a given specification. However, if model checking shows that the system model violates the specification, the designer has to manually refine the system model. To automate this refinement process, we propose a learning-based synthesis framework that can automatically eliminate all counterexamples from a system model based on causality semantics such that the synthesized model satisfies a given safety specification. Further, the framework for synthesis is not only automatic, but is also an iterative compositional process based on the L algorithm, i.e., the global state space of the system is never generated in the synthesis process. We also prove the correctness and termination of the synthesis framework. © 2014 Springer International Publishing Switzerland.