/ Tools / By

Morse Reseach group

Home
Members
Projects
Publications
Activities
Tools
Morse Lab

OptySim

OptySim is a tool for the analysis and optimization of heterogeneous systems whose behaviour can be observed as execution traces.

OptySim shares a common ancestor with TJT, a tool for testing Java programs using LTL.

Features

  • Based on the Spin model checker.
  • Analyzes systems observed as execution traces. Different types systems may be analyzed by implementing a communication protocol that provides the traces to OptySim. For instance, this has been used to analyze ns-2 network simulations. Our tool TJT follows a similar approach to test Java programs.
  • Supported properties: LTL formulas, asserts. Furthermore, properties can be tagged as positive or negative, to provide more information to the user. 
  • Parameterized analysis: the system under analysis may be parameterized and the user may provide ranges of values for these parameters. OptySim will generate all possible parameter configurations, execute the system using each configuration, and evaluate the given properties on each of them.

Download

Please send an e-mail to Alberto Salmerón (salmeron@lcc.uma.es).

References

  • A. Salmerón, “Model Checking Techniques for Runtime Testing and QoS Analysis.” Universidad de Málaga, Servicio de Publicaciones y Divulgación Científica, 2014.
  • A. Díaz, P. Merino, A. Salmeron, “Obtaining models for realistic mobile network simulations using real traces”, IEEE Communications Letters, vol. 15, no. 7, Piscataway, N. J., IEEE Communications Society, pp. 782–784, oct, 2011.
  • P. Merino, A. Salmeron, “Combining SPIN with ns-2 for protocol optimization”, Jaco van de Pol y Michael Weber (Eds.). Model checking software: 17th International SPIN workshop. Enschede, The Netherlands, September 27-29, 2010. Proceedings, Berlín, Springer, pp. 40–57, dec, 2010.

Contact