Advertisement

UFIT: A Tool for Modeling Faults in UPPAAL Timed Automata

  • Reza HajisheykhiEmail author
  • Ali Ebnenasir
  • Sandeep S. Kulkarni
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)

Abstract

We present the tool UFIT (Uppaal Fault Injector for Timed automata). In UFIT, we model five types of faults, namely, message loss, transient, byzantine, stuck-at, and fail-stop faults. Given the fault-free timed automata model and the selection of a type of fault, UFIT models the faults and generates the fault-affected timed automata model automatically. As a result, the designer can analyze the behavior of the model in the presence of faults. Moreover, there are several tools that extract timed automata models from higher-level programs. Hence, the designer can use UFIT to inject the faults into the extracted models.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Herber, P., Pockrandt, M., Glesner, S.: Transforming SystemC Transaction Level Models into UPPAAL timed automata. In: Singh, S., Jobstmann, B., Kishinevsky, M., Brandt, J. (eds.) MEMOCODE, pp. 161–170. IEEE (2011)Google Scholar
  2. 2.
    Olivero, A., Sifakis, J., Yovine, S.: Using abstractions for the verification of linear hybrid systems. In: Computer Aided Verification, CAV, pp. 81–94 (1994)Google Scholar
  3. 3.
    Lisherness, P., Cheng, K.T.: SCEMIT: a systemc error and mutation injection tool. In: Design Automation Conference, DAC, pp. 228–233 (2010)Google Scholar
  4. 4.
    Giovanni, B., Bolchini, C., Miele, A.: Multi-level fault modeling for transaction-level specifications. In: Great Lakes Symposium on VLSI, pp. 87–92 (2009)Google Scholar
  5. 5.
    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)Google Scholar
  6. 6.
    Springintveld, J., Vaandrager, F.W., D’Argenio, P.R.: Testing timed automata. Theor. Comput. Sci. 254 (1–2), 225–257 (2001)Google Scholar
  7. 7.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)Google Scholar
  8. 8.
    Summerfield, M.: Rapid GUI Programming with Python and Qt. Prentice Hall, California (2008)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Reza Hajisheykhi
    • 1
    Email author
  • Ali Ebnenasir
    • 2
  • Sandeep S. Kulkarni
    • 1
  1. 1.Michigan State UniversityEast LansingUSA
  2. 2.Michigan Technological UniversityHoughtonUSA

Personalised recommendations