Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code

International audienceblocks, and relies on a dataflow semantics: an (un)specified sampling time is used to trigger the computation. Every time step the whole model is evaluated and this computation is assumed to be instantaneous. This model of computation is particularly suited for discrete time dynamical systems such as time-triggered controllers. The use of models fitted with an executable semantics also enables early validation: the model can be simulated and evaluated with respect to its specification, before having the complete system. Ideally, the requirements would have to be checked with respect to the final embedded code. Two different approaches can be used for this purpose. The first one trusts the compilation process to preserve the model semantics in the produced code and the verification activities can be performed only-or mainly-at model level. This is the approach currently used in the industry when relying on qualified compilers such as SCADE KCG [28] or developed in academia with proved compilers such as CompCert [23] or verified Lustre compilers [8], [22]. In these approaches, the compiler implementation is complex and relies on the formalization of a proof of the compilation process based on the Curry-Howard isomorphism. A second approach, translation validation [29], [25], [26], authorizes to use of off-the-shelf compilers but requires the specification to be validated both at model and code level. This is the approach developed in this paper. We propose to rely on formal methods and perform exhaustive verification of requirements at all design stages of the development process. Our approach is specification oriented and requires specification to be formally defined as a logical component. Formal analyses are then performed at model level to ensure the verification of the specification. The model is next compiled to embeddable C code and its specification checked again at code level. The paper is structured as follows. Section II outlines the different approaches used to perform formal specification and verification. We also present basic algorithms used to support these verification activities. The next two sections focus on the model level: Section III addresses the formal specification of requirements at model level as well as the main principle behind model-checking, namely induction, while Section IV focuses specifically on the need to synthesize model invariants to support the verification activities. We present techniques to address the computation of non linear invariants using convex-based optimization. The last sections focus on code level: Abstract-In this paper, we outline a methodology allowing to support the formal verification o f f unctional p roperties for generated code. When relying on a code generator, a model is directly mapped into the target embedded code, in C for instance. At model level, a specification c an b e a ssociated to the model and used to assess the validity of the model with respect to its requirements. At code level, other means such as deductive methods can be used to ensure similar goals. While the analysis of user-specified p roperties a t m odel-level i s developed and tractable, the automatic verification o f t hese s pecification at code level remains an open issue. We present here a framework which builds a semantics layer connecting model specification to code specification, a s w ell a s a ssociated p roof evidences. This approach has been designed and developed in the context of dataflow languages such as Simulink, SCADE or Lustre, typically used in the design of cyber-physical system controllers, but it could also be revisited in other contexts. The model is analyzed by SMT-based model checking and convex optimization-based static analysis. At code level, deductive techniques, such as implemented in Frama-C, are used to prove the functional correctness. Our approach combines static analysis with refinement t o d rive the proof at code level, relying on analysis results obtained at model level. The refinement relates the initial model semantics with the one of the code. This papers only outlines the methodology combining analyses. It has been applied manually on some examples. A fully implementation remains a future work