Context Modelling and Partial-Order Reduction: Application to SDL Industrial Embedded Systems
Résumé
In this paper we introduce a method combining system environment description and partial-order reduction for the verification of SDL systems. The aim of this work is to identify a new independence relation in case of open reactive systems: a system communicating asynchronously with its surrounding environment (context). The environment contrains the system to some interesting configurations so that to reducce its behaviour. We show how to characterize the context as a set of traces which can explode when the environment is composed by several concurrent actors. We then propose a solution for its reduction gathering the traces into equivalent Mazurkiewicz classes so that to make such approach scalable. We apply this method on two avionics case study