Changes between Initial Version and Version 1 of RelatedTools

Timestamp:

10/04/10 12:22:57 (7 years ago)

Author:

mayer

Comment:

--

RelatedTools

@@ +1 @@
+= Related Tools =
+
+== SRML-Editor and Use Case Wizard ==
+
+Information: See http://www.pst.informatik.uni-muenchen.de:8080/Sensoria/WP+1 
+
+Update Site: http://www.cs.le.ac.uk/srml/milestone/update/site.xml 
+
+'''License:''' (not yet determined)
+
+||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts'''
+|| Modeling Environment for SENSORIA Reference Modelling Language (SRML)  ||  The SRML Modelling Environment a) allows textual modelling of SRML modules, b) provides editing functionalities (e.g., code completion), c) allows import/re-editing of existing SRML modules, d) allows to validate SRML modules with respect to the SRML meta-model and to store SRML models, e) allows to create graphical representation of SRML modules structure and to edit it. || Textual representation of SRML specifications Input || validated SRML textual models and graphical representations of their structure Output  || ULEICES: Laura Bocchi, Yi Hong
+|| SRML Use Case Wizard || The Use Case Wizard transforms an extension of Use Case diagrams with specialized actors to SRML textual specification and module diagram. ||  SRML Use Case diagrams  || SRML textual models specifications and modules diagrams || ULEICES: Laura Bocchi,  Yi Hong 
+
+== Process Calculi Term Visualization Tool (ADR2GRAPHS) ==
+
+Information: See http://www.albertolluch.com/adr/ 
+
+Download URL: http://www.albertolluch.com/adr2graphs/ 
+
+'''License:''' (not yet determined)
+
+||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts'''
+|| ADR2GRAPHS  ||  ADR2GRAPHS is a simple visualisator of algebraic specifications, including a graph algebra and the pi-calculus. It is based on part of the implementation of ADR (Architectural Design Rewriting) in the rewrite engine Maude.  || a term of the source language (graph algebra, pi-calculus, etc.).  || a graph in dot format (www.graphviz.org) and an image visualising the graph.  || PISA: Alberto Lluch Lafuente 
+
+== CareStudio / Sensoria Reengineering Environment ==
+
+'''License:''' Commercial.
+
+||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts'''
+|| CareStudio  ||  CareStudio is an Eclipse plugin that allows the creation, edition and execution of code pattern matching rules. The result is a report with the occurrences of each match for the given source code. || Source code  || Code pattern matching occurrences || ATX: Carlos Matos
+|| Sensoria Reengineering Environment || This tool (or set of tools) allows transformations to be applied to source code, with a focus on achieving SOA-compliant code. It consists of 4 steps: 1. CareStudio is used to execute code pattern matching rules; 2. a reverse engineering tool uses the source code and the information from 1. to produce a graph; an application generated from a Tiger EMF Transformer specification is used to transform the graph to adhere to the intended constraints, 4. a forward engineering application outputs the target code based on the transformations that were applied at model level. || Source code || Transformed source code || ATX: Carlos Matos
+
+== sCOWS Model Checker ==
+
+'''License:''' (not yet determined).
+
+||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts'''
+|| sCOWS Model Checker || This tool allows to perform statistical model checking on sCOWS, a stochastic extension of COWS. Taken a sCOWS model and a CSL formula as input, the tool produces an answer to the CSL formula with user-defined confidence. The computation is based on statistical reasoning on sCOWS simulation traces which are generated on the fly. || sCOWS models and CSL formulae || model checking results and formulae estimations || UNITN: Stefano Schivo. See http://disi.unitn.it/~schivo (follow the link "sCOWS Model Checker")
+
+== sCOWS to PRISM ==
+
+'''License:''' (not yet determined).
+
+||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts'''
+|| sCOWS Transition System and CTMC generator || This tool generates the transition system and the corresponding CTMC for a sCOWS service || sCOWS model || CTMC (in PRISM notation), Transition System (.dot format, useful to obtain a nice graphical representation) || UNITN: Igor Cappello. See http://disi.unitn.it/~cappello/index.php?vis=dl
+
+== ChorSLMC ==
+
+'''License:''' GNU General Public License (GPL) (http://www.gnu.org/licenses/gpl-3.0.txt)
+
+For more information, see http://ctp.di.fct.unl.pt/SLMC/
+
+||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts'''
+|| ChorSLMC || ChorSLMC is a verification tool for service-based systems that allows to verify choreography conformance, taking as input systems specified in Conversation Calculus, a core calculus for SOC developed within the SENSORIA project, and WS-CDL like choreographic descriptions. The tool is implemented as an extension to SLMC, a framework for model checking distributed systems against properties expressible in dynamic spatial logic, and may also be used on service-based systems to check other interesting properties of typical distributed systems, using the core dynamic-spatial logic available in SLMC. || Textual representation of the system and choreography (Conversation Calculus and WS-CDL like specifications, respectively) || Textual representation of the analysis result || FCTUNL: Hugo Torres Vieira
+
+== Venus ==
+
+For more information, see http://rap.dsi.unifi.it/cows/
+
+'''License:''' GNU General Public License (GPL) (http://www.gnu.org/licenses/gpl-3.0.txt) 
+
+||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts'''
+|| VENUS || VENUS is a Verification ENvironment for UML models of Services. This tool permits the verification of service properties by relying on (transparent) mathematically founded techniques. VENUS has been explicitly developed for being accessible by users not familiar with formal methods. Its theoretical bases are the calculus COWS, the temporal logic SocL and the model checker CMC. VENUS automatically translates UML4SOA models of services and natural language statements of service properties into, respectively, COWS terms and Socl formulae, and then checks them using CMC, possibly providing counterexamples. || UML4SOA Model || "OK" or Violation Trace || Francesco Tiezzi (http://rap.dsi.unifi.it/~tiezzi/)
+
+== BliteC ==
+
+For more information, see URL: http://rap.dsi.unifi.it/blite 
+
+'''License:''' LGNU General Public License (GPL) (http://www.gnu.org/licenses/gpl-3.0.txt) 
+
+||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts'''
+|| BliteC || BliteC is a software tool for supporting a rapid and easy development of WS-BPEL applications. BliteC translates service orchestrations written in Blite, a formal language inspired to but simpler than WS-BPEL, into executable WS-BPEL programs. The tool simplifies the task of developing WS-BPEL applications because Blite provides a textual programming notation and is equipped with an unambiguous semantics, while BliteC properly packages the produced files to be readily deployed and executed in a WS-BPEL engine. || BLite || BPEL || Francesco Tiezzi (http://rap.dsi.unifi.it/~tiezzi/)