| dc.description.abstract | Automated code-generators are increasingly becoming the workhorses in model-based development of Cyber-Physical Systems (CPS). Significant model-driven tools have emerged incorporating advanced model-checking methods that can provide some assurance regarding the quality and correctness of the models. However, the code generated from these models still remains circumspect, since the correctness of the code-generators cannot be assumed as a given. Therefore, to increase trust in the code-generators formal verification of their correctness is paramount. Manual verification of entire code-generators under all possible context and inputs is a daunting task, considering the complexity and size of code-generators. We are proposing a pragmatic approach for ascertaining correctness of code-generators that, instead of verifying their explicit implementation, verifies the correctness of the generated code with respect to a specific set of user-defined properties to establish that the code-generators are property-preserving.
In this thesis, we discuss an existing model-based design method for compositional synthesis of CPS and show the integration of a toolchain with it, which provisions an automated verification workflow for proving correctness of the code generated by code-generators in an iterative fashion. In order to make the verification workflow conducive to domain engineers, who are not often trained in formal methods, we include a mechanism for high-level specification of temporal properties using pattern-based verification templates. The presented toolchain leverages state-of-the-art verification tools. We illustrate the approach of presented toolchain with a case-study of an Ignition Logic Controller of an automotive vehicle. | |
