Modelling and Evaluation of a Satellite System Using EVAL*, a Petri Net Based Industrial Tool

This paper reports an experiment conducted with EVAL, a Petri Nets based tool, on a satellite application. The satellite architecture is described, using EVAL specification language which provides powerful communication mechanisms (multi-rendez-vous) along with modular decomposition. In addition to interactive behaviour simulation, the tool supports exhaustive analysis techniques, with respect to logical, temporal or stochastic criteria of the system. Verification results on the satellite application are presented. We stress on the use of a modelling methodology to build analysis models.