A Platform-Based Approach to Verification and Synthesis of Linear Temporal Logic Specifications

The design of Cyber-Physical Systems (CPS) is challenging as it requires coordination across several domains (e.g., functional, temporal, mechanical). To cope with complexity, rarely a CPS is built from scratch. Instead, it is assembled by reusing available components and subsystems. If a component is not available, then it is made to order according to a specification which ensures its compatibility with the rest of the system.To achieve design goals faster while guaranteeing system safety, the correct instantiation of modules and subsystems is essential. Formal specifications, such as those expressed in Linear Temporal Logic (LTL), have the potential to drastically reduce design and implementation efforts by enabling rigorous requirement analysis and ensuring the correct composition of reusable designs. Composing formal specifications, however, is a tedious and error-prone activity, and the scalability of existing formal analysis techniques is still an issue. In this dissertation, we present a set of techniques and algorithms that leverage compositional design principles to enable faster verification and correct-by-construction, platform-based synthesis of LTL specifications. In our framework, a design is a composition of several components (which could describe both hardware and software elements) represented through their specifications, expressed as LTL assume/guarantee interfaces, or contracts. The collection of all the available contracts, i.e., a library, describes the design platform. The contracts in the library are the building blocks of different possible designs, and they are simple enough that their correctness can be easily verified, yet complete enough to guarantee the correct and safe use of the components they represent. Our contribution is two-fold. On the one hand, we address the verification task: given an existing composition of contracts from the library, we want to check whether it satisfies a set of desired requirements. We improve the scalability of existing verification techniques by leveraging pre-verified relations between contracts in the library. On the other hand, we enable specification synthesis: given a (possibly incomplete) set of desired system properties, we are able to automatically generate a composition of contracts, chosen from a library, that satisfies them. We do so by devising a set of algorithms based on formal inductive synthesis, where a candidate is either accepted as correct or is used to infer new constraints and guide the synthesis process towards a solution. Additionally, we show how to increase the scalability of our approach by leveraging principles from the contract framework to decompose a synthesis problem into several independent tasks, which are simpler than the original problem. We validate our work by applying it to several industrial-relevant case studies, including the problem of verification and synthesis of a controller for the electrical power system of an aircraft