|
Additional tools were developed whithin the scope of the SENSORIA project. The integration iof these tools in the SENSORIA Development Environment is work in progress. - SRML-Editor and Use Case Wizard
The Modeling Environment for SENSORIA Reference Modelling Language (SRML)
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.
The SRML Use Case Wizard transforms an extension of Use Case diagrams with specialized actors to SRML textual specification and module diagram.
License: not determined yet
URL:http://www.pst.informatik.uni-muenchen.de:8080/Sensoria/WP+1,
http://www.cs.le.ac.uk/srml/milestone/update/site.xml
- Process Calculi Term Visualization Tool (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.
License: not determined yet
URL: http://www.albertolluch.com/adr/, http://www.albertolluch.com/adr2graphs/
- Care Studio / Sensoria Reengineering Environment
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.
Sensoria Reengineering Environment (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. License: commercial
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. License: not determined yet
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. License: GNU General Public License (GPL) (http://www.gnu.org/licenses/gpl-3.0.txt) URL: http://ctp.di.fct.unl.pt/SLMC/
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.
License: GNU General Public License (GPL) (http://www.gnu.org/licenses/gpl-3.0.txt)
URL:http://rap.dsi.unifi.it/cows/
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.
License: GNU General Public License (GPL) (http://www.gnu.org/licenses/gpl-3.0.txt)
URL: http://rap.dsi.unifi.it/blite
|
