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/)