Difference between revisions of "Maude Tools"

From The Maude System
Jump to: navigation, search
(5 intermediate revisions by the same user not shown)
Line 1: Line 1:
 
Formal tools for Maude specifications
 
Formal tools for Maude specifications
* [https://code.google.com/p/maude-formal-environment/ The Maude Formal Environment] - Environment that integrates the Church-Rosser checker, the coherence checker, and the termination tool
+
* [https://github.com/maude-team/MFE/wiki The Maude Formal Environment] - Environment that integrates the Church-Rosser checker, the coherence checker, and the termination tool
 
* [http://maude.cs.uiuc.edu/tools/tlr/ The Maude LTLR Model Checker]
 
* [http://maude.cs.uiuc.edu/tools/tlr/ The Maude LTLR Model Checker]
 
* [http://maude.cs.uiuc.edu/tools/lmc/ The Maude LTL Logical Model Checker]
 
* [http://maude.cs.uiuc.edu/tools/lmc/ The Maude LTL Logical Model Checker]
 
* [http://maude.cs.uiuc.edu/tools/pvesta/index.html PVeStA] - A Parallel Statistical Model Checking and Quantitative Analysis Tool
 
* [http://maude.cs.uiuc.edu/tools/pvesta/index.html PVeStA] - A Parallel Statistical Model Checking and Quantitative Analysis Tool
 +
* [http://sysma.imtlucca.it/tools/multivesta/ MultiVeStA] - A Distributed Statistical Model Checking for Discrete Event Simulators
 
* [http://maude.cs.uiuc.edu/tools/itp/ Inductive Theorem Prover (ITP)]
 
* [http://maude.cs.uiuc.edu/tools/itp/ Inductive Theorem Prover (ITP)]
 
* [http://maude.cs.illinois.edu/tools/scc/ Sufficient Completeness Checker]
 
* [http://maude.cs.illinois.edu/tools/scc/ Sufficient Completeness Checker]
* [http://maude.cs.uiuc.edu/tools/rtp/ The Maude Resolution Theorem Prover (RTP)]
+
<!-- * [http://maude.cs.uiuc.edu/tools/rtp/ The Maude Resolution Theorem Prover (RTP)] -->
* [http://maude.cs.uiuc.edu/tools/Maude-NPA/index.html Maude-NPA] - Maude-NRL Protocol Analyzer
+
<!-- * [http://maude.cs.uiuc.edu/tools/Maude-NPA/index.html Maude-NPA] - Maude-NRL Protocol Analyzer -->
 +
* [[Maude Tools: Maude-NPA|Maude-NPA]] - Maude-NRL Protocol Analyzer
 
* [http://maude.cs.illinois.edu/tools/eq-enrich/ Equality Enrichments for Order-Sorted Maude Theories]
 
* [http://maude.cs.illinois.edu/tools/eq-enrich/ Equality Enrichments for Order-Sorted Maude Theories]
* [[Maude Tools:Order-sorted Term Patterns|Order-sorted Term Patterns]] - A tool to discover term patterns
+
* [[Maude Tools: Order-sorted Term Patterns|Order-sorted Term Patterns]] - A tool to discover term patterns
 
* [http://maude.cs.uiuc.edu/tools/createcinni createCINNI] - Automatic Generation of CINNI Instances for the Maude System
 
* [http://maude.cs.uiuc.edu/tools/createcinni createCINNI] - Automatic Generation of CINNI Instances for the Maude System
  
 
Extensions of Maude
 
Extensions of Maude
* [http://heim.ifi.uio.no/~peterol/RealTimeMaude/ Real-Time Maude]
+
* [https://olveczky.se/RealTimeMaude/ Real-Time Maude]
 
* [http://maude.sip.ucm.es/strategies/index.html Maude Strategy Language]
 
* [http://maude.sip.ucm.es/strategies/index.html Maude Strategy Language]
 
* [http://safe-tools.dsic.upv.es/acuos/ ACUOS]. Order-Sorted Modular ACU (Least General) Generalization System
 
* [http://safe-tools.dsic.upv.es/acuos/ ACUOS]. Order-Sorted Modular ACU (Least General) Generalization System

Revision as of 23:01, 9 February 2021

Formal tools for Maude specifications

Extensions of Maude

Tools to assist in the development of Maude specifications

Tools for other formalisms and logics developed on Maude

Semantics and verification of programming languages

Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...)

  • MR-SynchAADL - Multirate Synchronous AADL and the MR-SynchAADL tool
  • MOMENT - A framework for model management
  • e-Motions - Visual definition of domain-specific modeling languages
  • mOdCL - UML/OCL specification, with static and dynamic evaluation of OCL expressions
  • Web-TLR. A Model Checker for Web applications using LTLR

Other tools: