Advertisement

Abstract

Real-Time Maude is a rewriting-logic-based tool supporting the formal specification and analysis of real-time systems. Our tool emphasizes expressiveness and ease of specification over algorithmic decidability of key properties, and provides a spectrum of analysis methods, including symbolic simulation, and unbounded and time-bounded reachability analysis and LTL model checking. Real-Time Maude has proved well suited to analyze both correctness and performance of large and complex real-time systems, including state-of-the-art schedulers, network protocols, and wireless sensor network algorithms.

Keywords

Sensor Node Wireless Sensor Network Model Check Linear Temporal Logic Multicast Protocol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  2. 2.
    Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)zbMATHCrossRefGoogle Scholar
  3. 3.
    Ölveczky, P.C., Meseguer, J.: Specification and analysis of real-time systems using Real-Time Maude. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 354–358. Springer, Heidelberg (2004)Google Scholar
  4. 4.
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, Springer, Heidelberg (1998)Google Scholar
  5. 5.
    Ölveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. Electronic Notes in Theoretical Computer Science 176(4), 5–27 (2007)CrossRefGoogle Scholar
  6. 6.
    Ölveczky, P.C., Grimeland, M.: Formal analysis of time-dependent cryptographic protocols in Real-Time Maude. In: IPDPS 2007, IEEE, Los Alamitos (2007)Google Scholar
  7. 7.
    Lien, E.: Formal modelling and analysis of the NORM multicast protocol using Real-Time Maude. Master’s thesis, Dept.of Linguistics, University of Oslo (2004)Google Scholar
  8. 8.
    Katelman, M., Meseguer, J., Hou, J.: Formal modeling, analysis, and debugging of a wireless sensor network protocol with Real-Time Maude and statistical model checking. Technical report, Dept.of Computer Science, University of Illinois at Urbana-Champaign (In preparation, 2008)Google Scholar
  9. 9.
    Kim, M., Dutt, N., Venkatasubramanian, N.: Policy construction and validation for energy minimization in cross layered systems: A formal method approach. In: IEEE RTAS 2006 (2006)Google Scholar
  10. 10.
    Ölveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. Formal Methods in System Design 29, 253–293 (2006)zbMATHCrossRefGoogle Scholar
  11. 11.
    Ölveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In: Baresi, L., Heckel, R. (eds.) FASE 2006 and ETAPS 2006. LNCS, vol. 3922, pp. 357–372. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Ölveczky, P.C., Thorvaldsen, S.: Formal modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 122–140. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Peter Csaba Ölveczky
    • 1
  • José Meseguer
    • 2
  1. 1.Department of InformaticsUniversity of Oslo 
  2. 2.Department of Computer ScienceUniversity of Illinois at Urbana-Champaign 

Personalised recommendations