Difference between revisions of "Maude Tools"

From The Maude System
Jump to: navigation, search
Line 1: Line 1:
Formal tools for Maude specifications
+
== Formal tools for Maude specifications ==
 
* [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
 
* [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]
 +
* [https://github.com/fadoss/umaudemc umaudemc] - A unified tool to check Maude specifications using external qualitative, probabilistic, and stochastical model checkers
 
* [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://sysma.imtlucca.it/tools/multivesta/ MultiVeStA] - A Distributed Statistical Model Checking for Discrete Event Simulators
Line 14: Line 15:
 
* [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==
 
* [https://olveczky.se/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
  
Tools to assist in the development of Maude specifications
+
==Tools to assist in the development of Maude specifications==
 
* [http://maude.sip.ucm.es/debugging/ Declarative Debugger]
 
* [http://maude.sip.ucm.es/debugging/ Declarative Debugger]
 
* [http://safe-tools.dsic.upv.es/anima/ The Anima tool] - Stepwise inspection of Maude computations
 
* [http://safe-tools.dsic.upv.es/anima/ The Anima tool] - Stepwise inspection of Maude computations
Line 25: Line 26:
 
* [http://safe-tools.dsic.upv.es/iJulienne/ iJulienne]. Backward Trace Slicer
 
* [http://safe-tools.dsic.upv.es/iJulienne/ iJulienne]. Backward Trace Slicer
  
Tools for other formalisms and logics developed on Maude
+
==Tools for other formalisms and logics developed on Maude==
 
* [http://pl.csl.sri.com/ Pathway Logic Assistant] - Modeling of biological entities and processes
 
* [http://pl.csl.sri.com/ Pathway Logic Assistant] - Modeling of biological entities and processes
 
* [http://fsl.cs.illinois.edu/index.php/Circ Circ] - An automated behavioral prover based on the circularity principle
 
* [http://fsl.cs.illinois.edu/index.php/Circ Circ] - An automated behavioral prover based on the circularity principle
Line 31: Line 32:
 
* [http://maude.cs.uiuc.edu/maude1/casestudies/ccs CCS] and [http://maude.sip.ucm.es/~alberto/esf LOTOS]
 
* [http://maude.cs.uiuc.edu/maude1/casestudies/ccs CCS] and [http://maude.sip.ucm.es/~alberto/esf LOTOS]
  
Semantics and verification of programming languages
+
==Semantics and verification of programming languages==
 
* [https://github.com/fcbr/mmt Maude MSOS tool]
 
* [https://github.com/fcbr/mmt Maude MSOS tool]
 
* [http://fsl.cs.illinois.edu/index.php/K_and_Matching_Logic The K framework and Matching logic] - Rewrite-based framework for the definition of formal operational semantics of programming languages
 
* [http://fsl.cs.illinois.edu/index.php/K_and_Matching_Logic The K framework and Matching logic] - Rewrite-based framework for the definition of formal operational semantics of programming languages
Line 38: Line 39:
 
* [http://maude.cs.uiuc.edu/tools/javaitp Java+ITP] - A tool to prove Java properties
 
* [http://maude.cs.uiuc.edu/tools/javaitp Java+ITP] - A tool to prove Java properties
  
Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...)
+
==Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...)==
 
* [http://maude.cs.illinois.edu/tools/synchaadl/ MR-SynchAADL] - Multirate Synchronous AADL and the MR-SynchAADL tool
 
* [http://maude.cs.illinois.edu/tools/synchaadl/ MR-SynchAADL] - Multirate Synchronous AADL and the MR-SynchAADL tool
 
* [http://moment.dsic.upv.es/ MOMENT] - A framework for model management
 
* [http://moment.dsic.upv.es/ MOMENT] - A framework for model management
Line 45: Line 46:
 
* [http://zenon.dsic.upv.es:8080/webtlr/ Web-TLR]. A Model Checker for Web applications using LTLR
 
* [http://zenon.dsic.upv.es:8080/webtlr/ Web-TLR]. A Model Checker for Web applications using LTLR
  
Other tools:
+
==Other tools==
 +
* [https://github.com/fadoss/maude-bindings Python's library] Language bindings to use Maude from other programming languages like Python
 
* [http://www.lcc.uma.es/~duran/MTT Maude Termination Tool]
 
* [http://www.lcc.uma.es/~duran/MTT Maude Termination Tool]
 
* [http://www.lcc.uma.es/~duran/ChC Coherence Checker]
 
* [http://www.lcc.uma.es/~duran/ChC Coherence Checker]

Revision as of 14:42, 29 March 2022

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