Formalization of software models for cyber-physical systems.

ABSTRACT The involvement of formal methods is indispensable for modern software engineering. This especially holds for Cyber-Physical Systems (CPS). In order to deal with the complexity and heterogeneity of the design, model-based engineering is widely used. The complexity of detailed verification in the final source code makes it imperative to introduce formal methods earlier in the design process. Because of the widespread use of customized modeling languages (domain-specific modeling languages, DSMLs), it is crucial to formally specify the DSML, and verify if the model meets fundamental correctness criteria. This is achieved by specifying behavioral and structural semantics of the modeling language. 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, using auto code generators remains circumspect, since the correctness of the code generators cannot be assumed as a given, and remains intractable to prove. Therefore, we propose a pragmatic approach, instead of verifying explicit implementation of code generator, 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 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, and a small case-study illustrates the approach.