Expressing and implementing operational profiles for reactive software validation

Lutess is a tool that we developed for testing reactive synchronous software and which is being used in different industrial contexts. It offers several formal testing methods with automatic generation of test data from the environment specification. Lutess provides also an approach to assign a probability to the next event issued by the environment. However, a Lutess´ user faces the problem of expressing operational profiles with sophisticated and varying probability assignments to software inputs, in a format directly usable by Lutess. The paper concentrates on how to express operational profiles for specifications which are implemented as binary decision diagrams