Verification of design contracts for cyber-physical system design using evolutionary optimization

Cyber-Physical Systems (CPS) have enabled plethora of applications and are seen as future solutions to build large-scale infrastructure. Controller meeting design requirements and performance objectives are required for building CPS. This is non-trivial due to the interplay and temporal constraints among the physical, computing, communication, and control entities within CPS. This paper presents design contracts (an agreement) between software, network and control engineers to build CPS controllers. Jitter bounds are used to synthesize the design contract that are verified by solving multiobjective optimization problem (MOP) to specify temporal parameter (jitter bound) and also guarantee performance. To solve the MOP, NSGA-II is used (Nondominated sorting genetic algorithm) due to its ability to generate non-dominated solutions; a desirable feature for design involving tradeoff. The synthesis and verification procedure is illustrated using experiments with simple example.