Evaluating Behavior Correctness of Synchronous Systems through Time to Service Distribution Analysis: Tools Required

For synchronous software validation, in addition to safety properties, eventuality properties may be required to specify that a request will be eventually served. Even if the eventuality properties are true, a deeper analysis of the "time-to-service" (time between a request and its response) under different environmental conditions can bring additional information about the system behavior correctness. The paper underlines the need of tools easy-to-use which could help to carry out such kind of analyses.