Difference between revisions of "Maude Tools"
From The Maude System
Maudesystem (Talk | contribs) |
Maudesystem (Talk | contribs) |
||
Line 15: | Line 15: | ||
* [http://heim.ifi.uio.no/~peterol/RealTimeMaude/ Real-Time Maude] | * [http://heim.ifi.uio.no/~peterol/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 | ||
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 | ||
+ | * [http://safe-tools.dsic.upv.es/abets/ ABETS]. Assertion-based, Maude dynamic analyzer | ||
+ | * [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 | ||
Line 33: | Line 36: | ||
* [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 | ||
− | 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 | ||
* [http://atenea.lcc.uma.es/e-motions e-Motions] - Visual definition of domain-specific modeling languages | * [http://atenea.lcc.uma.es/e-motions e-Motions] - Visual definition of domain-specific modeling languages | ||
* [http://maude.lcc.uma.es/mOdCL/ mOdCL] - UML/OCL specification, with static and dynamic evaluation of OCL expressions | * [http://maude.lcc.uma.es/mOdCL/ mOdCL] - UML/OCL specification, with static and dynamic evaluation of OCL expressions | ||
+ | * [http://zenon.dsic.upv.es:8080/webtlr/ Web-TLR]. A Model Checker for Web applications using LTLR | ||
Other tools: | Other tools: |
Revision as of 10:25, 14 May 2015
Formal tools for Maude specifications
- The Maude Formal Environment - Environment that integrates the Church-Rosser checker, the coherence checker, and the termination tool
- The Maude LTLR Model Checker
- The Maude LTL Logical Model Checker
- PVeStA - A Parallel Statistical Model Checking and Quantitative Analysis Tool
- Inductive Theorem Prover (ITP)
- Sufficient Completeness Checker
- The Maude Resolution Theorem Prover (RTP)
- Maude-NPA - Maude-NRL Protocol Analyzer
- Equality Enrichments for Order-Sorted Maude Theories
- Order-sorted Term Patterns - A tool to discover term patterns
- createCINNI - Automatic Generation of CINNI Instances for the Maude System
Extensions of Maude
- Real-Time Maude
- Maude Strategy Language
- ACUOS. Order-Sorted Modular ACU (Least General) Generalization System
Tools to assist in the development of Maude specifications
- Declarative Debugger
- The Anima tool - Stepwise inspection of Maude computations
- ABETS. Assertion-based, Maude dynamic analyzer
- iJulienne. Backward Trace Slicer
Tools for other formalisms and logics developed on Maude
- Pathway Logic Assistant - Modeling of biological entities and processes
- Circ - An automated behavioral prover based on the circularity principle
- OCC - An Open Calculus of Constructions
- CCS and LOTOS
Semantics and verification of programming languages
- Maude MSOS tool
- The K framework and Matching logic - Rewrite-based framework for the definition of formal operational semantics of programming languages
- JavaRL Rewriting specification of a Java semantics - Java interpreter and formal analysis
- JavaFAN - Executable rewrite logic semantics of both Java and Java Bytecode using Maude
- Java+ITP - A tool to prove Java properties
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: