The following are a number of open source software products disseminating outcome of our research as proof of concept:

  • NL2OCLviaSBVR: Despite a decade of research in academia, OCL is seen as the least adopted member of the UML family of languages. Use of OCL can result in elegant design of software, reduction of complexity and paves the way for the application of formal methods techniques to software. The poor uptake of OCL is often attributed to its syntax. NL2OCLvia SBVR is a set of tools that create SBVR business vocabulary, SBVR business rules, OCL constraints and Alloy expression from Natural Language (such as English) specification. read more …

  • Simple Transformer (SiTra): An MDD environment written in Java, SiTra allows specification of transformations in Java and embodies a powerful engine for the execution of transformations. SiTra has been used in numerous applications, including UML2Alloy, NL2OCLviaSBVR, StateMachine to VHDL, BPEL to OWLs, Automatic generation of Diagnosers/Monitors in SoA. read more …

  • UML2Alloy: a tool for automated transformation of models created in UML class diagrams and OCL to Alloy models. The Alloy model can be automatically analysed, hence the approach bridges the gap between design and analysis by allowing analysis of UML models via Alloy (with the help of SAT-solvers). read more …

  • AC2Alloy&TA: is the outcome of a research which attempts to model Access Control Specification in the context of Spatio-Temporal Role Based Access Control using formal methods (Alloy & Timed Automata), Thus allowing for powerful automatic analysis to be carried out for detecting undesirable scenarios such as occurrence of inconsistencies. read more …

  • QVT2SiTra: a model transformation solution to implementing Relational QVT in Java Supporting the developers in designing, maintaining and implementing Transformation rules is a key challenge of Model Driven Architecture. Relational QVT (Query/View/Transformation) is a declarative model transformation language supported… read more …

  • Time Action Lock Checker (TALC): A tool for detecting deadlocks and time-action locks in Timed Automate models via using Rational Presburger Arithmetic (RPA). TALC is created in collaboration with University of Osaka, Japan, and embodies an implementation of the fastest available RPA algorithm. read more …

  • Dblue : A transparent, fault-tolerant JDBC drive for connection via Bluetooth, which facilitates development of m-commerce applications such as various types of e-wallets.