Hao Wu

Cyclone

Cyclone is a new specification language for verifying/testing graph-based structures. Unlike other tools, Cyclone uses simple notations and allows users to build verification tasks by building graphs. Cyclone promotes the idea of thinking in graph, and makes verification tasks easy to be understood, visualised and learned for those who do not have verification background. Try Cyclone online here.

Papers:

Hao Wu and Zheng Cheng Verifying Event-B Hybrid Models using Cyclone 9th International Conference on Rigorous State Based Methods (ABZ), 2023 (DOI, PDF)

Cyclone Online

QMaxUSE

QMaxUSE is an automated verification tool that is able to verify consistencies of a UML class diagram annotated with OCL invariants. QMaxUSE has two distinct features: (1) A query langauge that allows users to select parts of class diagram to be verified. (2) A powerful algorithm that is capable of performing concurrent verification on large number of complex OCL invariants. This is achieved by decomposing a large model into multiple queries.

Papers:

Hao Wu. QMaxUSE: A New Tool for Verifying UML Class Diagrams and OCL Invariants Science of Computer Programming (SCP) - Software Track, 2023.

Hao Wu. QMaxUSE: A Query-based Verification Tool for UML Class Diagrams with OCL Invariants 25th International Conference on Fundamental Approaches to Software Engineering (FASE - ETAPS), 2022 (DOI, PDF)

[1] Hao Wu. A Query-based Approach for Verifying UML Class Diagrams with OCL Invariants 18th European Conference on Modelling Foundations and Applications (ECMFA - STAF), 2022 (in the special issue of Journal of Object Technology) (DOI, PDF)

Web

MaxUSE

MaxUSE is an automatic tool that finds the set of achievable features and constraint conflicts for inconsistent metamodels (UML class diagrams). MaxUSE allows users to freely rank individual model features or use automatic ranking. MaxUSE integrates USE modelling tool with Z3 SMT Solver. It currently uses Uran as its solving engine to interact with Z3.

Papers:

Hao Wu and Marie Farrell. A Formal Approach to Finding Inconsistencies in a Metamodel Software and Systems Modeling (SoSyM) , Jan, 2021. (DOI, PDF).

Hao Wu. MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams 13th International Conference on integrated Formal Methods (iFM), 2017 (DOI, PDF).

Hao Wu. Finding Achievable Features and Constraint Conflicts for Inconsistent Metamodels 13th European Conference on Modeling Foundations and Application (ECMFA@STAF), 2017 (DOI, PDF).

Web

Uran

Uran provides Java APIs for generating standard SMT2 formulas. Though Z3 Java API does the same thing, Uran differs by giving full control of generated SMT formulas. Thus, it is very well suited for debugging purpose. Currently, uran supports generating different kinds of formulas including: boolean-circuit gate (CNF), quantifiers, arithmetic (linear inequalities.). It now uses Z3 as its back-end solver. Uran can be considered as an engine that you could place in between solvers and your own specification language, and seperate your code from underlying solvers.

Web

ASMIG

ASMIG (A Small Metamodel Instance Generator) is a tool that I developed during my PhD. This tool is fully automatic and generates metamodel instances with respects to different kinds of OCL constraints. This tool is purely written in Java. It uses Eclipse EMF APIs to parse a metamodel and Z3 SMT Solver to solve the necessary constraints.

Papers:

Hao Wu. Generating Metamodel Instances Satisfying Coverage Criteria via SMT Solving 4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD), 2016 (DOI, PDF).

Hao Wu, Rosemary Monahan and James F. Power. Exploiting Attributed Type Graphs to Generate Metamodel Instances using an SMT Solver 7th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2013 (DOI, PDF).

Web