This page contains a list of the tool suites which have been integrated into the SDE. Each comes with its own UI, and an integration API to be usable via the SDE orchestration mechanisms. Further information and updates available ... - MDD4SOA Transformations and Analysis
The MDD4SOA transformers are a set of EMF transformers for converting UML4SOA models into target languages (supported are BPEL/WSDL, Java, and Jolie.), transformer for converting BPEL/WSDL to executable BPEL/WSDL and deployment, and an analysis tool for verifying that an orchestration conforms to its protocol.
URL: http://www.mdd4soa.eu/, http://www.jolie-lang.org
- LTSA / WS-Engineer / Dino Broker (Analysis)
LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour. WS-Engineer is an extension to LTSA which allows service models to be described by translation of the service process descriptions, and can be used to perform model-based verification of Web service compositions. Dino provides a mechanism for semantic dynamic service discovery.
Sensoria Reference Markovian Calculus (SRMC) is an extension to PEPA. The tool covers steady-state analysis of the underlying Markov chain of SRMC descriptions. The plug-in is a software tool that supports the stochastic process algebra PEPA, a formal language which allows quantitative analysis of systems. SRMC/UML complements SRMC offering facilities for meta-model transformations. It translates a subset of UML2 models (interactions and state machines) into an SRMC description for performance evaluation. Results are reflected back into the UML model. - VIATRA2 and Deployment Transformations (Model Transformation)
The main objective of the VIATRA2 (VIsual Automated model TRAnsformations) framework is to provide a general-purpose support for the entire life-cycle of engineering model transformations including the specification, design, execution, validation and maintenance of transformations within and between various modelling languages and domains. The UML2Axis transformations take high level UML4OA models and produce WSDL (Web Services Description Language), WS-Security and Apache Axis-specific configuration files as output. - CMC - UMC UCTL/Socl model checkers, and analysers
CMC model checker and analyser for systems defined by interacting UML statecharts. Allows to model-check on the fly abstract behavioral properties in the Socl braching-time state-action based, parametric temporal logic (all versions). Allows to explore the model evolution (all versions but SENSORIA SDE plugin). Allows to generate abstract full-trace minimized graphs of the system (only the online versions) UMC model checker and analyser for systems defined by interacting UML statecharts. Allows to model-check on the fly abstract behavioral properties in the Socl braching-time state-action based, parametric temporal logic (all versions). Allows to explore the model evolution (all versions but SENSORIA SDE plugin). Allows to generate abstract full-trace minimized graphs of the system (only the online versions) License: GNU General Public License (GPL) (http://www.gnu.org/licenses/gpl-3.0.txt) URL: http://fmt.isti.cnr.it/umc/UMCDISTR/Eclipsetools/it.cnr.isti.eclipsetools.update; http://fmt.isti.cnr.it/umc/ http://fmt.isti.cnr.it/cmc/- LYSA Tool - static protocol analyzer
Static analyzer for security protocols defined in the LYSA process calculus. Provides a prototype LYSA editor to assist users in the modeling of protocols. Given a LYSA model the analyzer will verify properties related to secrecy and authentication. License: Copyright University of Denmark URL: http://lbt.imm.dtu.dk/Sensoria/update; http://www.imm.dtu.dk/English/Research/Language-Based_Technology/Software/LySaTool.aspx Hugo/RT is a UML model translator for model checking, theorem proving, and code generation. A UML model containing active classes with state machines, collaborations, interactions, and OCL constraints can be translated into the system languages of the real-time model checker UPPAAL, the on-the-fly model checker SPIN, and into Java and SystemC code. License: not yet determined
|
