Performance verification of discrete event systems using hybrid model-checking

The results generated over the past few years on the formal verification of both Discrete Event Systems (DES) and Hybrid Dynamic Systems (HDS) are quite substantial, especially as regards the controller's properties of liveness and safety. In this paper, we will study the range of possibilities offered using the model-checking techniques in order to evaluate DES performances (in terms of quality of service provided by the automated system). This task calls for proceeding with a model-based approach that couples a hybrid model of the plant with a timed discrete model of the controller. We will also show, using a basic example, that by parameterizing the hybrid process model, the model-checker may then be employed to evaluate the robustness of the discrete control to perturbations encountered by the plant.