• AADL

  • Referenced in 4 articles [sw20835]
  • semantics of Multirate Synchronous AADL in Real-Time Maude, and integrate Real-Time Maude verification...
  • SynchAADL2Maude

  • Referenced in 4 articles [sw13325]
  • Eclipse plug-in that uses Real-Time Maude to simulate and model check Synchronous AADL ... modeling and verifying an asynchronous distributed real-time system that should be virtually synchronous...
  • PVeStA

  • Referenced in 18 articles [sw08423]
  • scalability of analysis available to tools like Maude, where probabilistic systems can be specified ... supports statistical model checking of probabilistic real-time systems specified as either: (i) discrete ... Chains; or (ii) probabilistic rewrite theories in Maude. Furthermore, the properties that it can model...
  • MOMENT2

  • Referenced in 10 articles [sw10025]
  • real-time rewrite formal semantics to real-time model transformations, and show how the models ... simulated and model checked using MOMENT2’s Maude-based analysis tools. In this way, MOMENT2 ... specifying and verifying model-based real-time and embedded systems within the Eclipse Modeling Framework...
  • Dist-Orc

  • Referenced in 5 articles [sw10063]
  • that allows structured programming of distributed and timed computations. Several formal semantics have been proposed ... Maude that narrows this gap considerably. The enabling feature of this technique is Maude ... calls and returns, and to provide real-time timing information to Orc expressions and sites...
  • ACL2

  • Referenced in 291 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1906 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Isabelle

  • Referenced in 719 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • PRISM

  • Referenced in 454 articles [sw01186]
  • PRISM: Probabilistic symbolic model checker. In this paper...
  • ML

  • Referenced in 524 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • Stratego

  • Referenced in 78 articles [sw01259]
  • Stratego/XT is a language and toolset for program...
  • Kronos

  • Referenced in 274 articles [sw01270]
  • KRONOS is a tool developed with the aim...
  • FoCs

  • Referenced in 20 articles [sw01591]
  • FoCs -- automatic generation of simulation checkers from formal...
  • JavaFAN

  • Referenced in 32 articles [sw01934]
  • Formal analysis of Java programs in JavaFAN. JavaFAN...
  • ELAN

  • Referenced in 108 articles [sw02179]
  • The ELAN system provides an environment for specifying...
  • CASL

  • Referenced in 174 articles [sw02235]
  • The specification language developed by CoFI is called...
  • ITP/OCL

  • Referenced in 7 articles [sw02727]
  • ITP/OCL: A rewriting-based validation tool for UML...
  • LOTOS

  • Referenced in 152 articles [sw02961]
  • Introduction to the ISO specification language LOTOS. LOTOS...
  • HOL/SPIN

  • Referenced in 24 articles [sw02987]
  • Routing information protocol in HOL/SPIN We provide a...