Application of partial-order methods for the verification of closed-loop SDL systems
Xavier Dumas, Philippe Dhaussy, Frédéric Boniol, Eric Bonnafous · 2011
This article is concerned with the verification of closed-loop asynchronous reactive systems. Such systems, specified for instance with the industrial SDL (Specification and Description Language) language, communicate with their environment through buffers which memorize occurrences of events. Such a communication mechanism is quite interesting for specifying systems connected to several asynchronous external actors. However, it leads to a verification model possibly composed of a huge number of states (due to the state-space of the buffers). This article shows how this combinatorial explosion could be reduced by specifying the environment of the system to be verified, and by using partial-orders methods both on the system and its environment.