Speaker: Dr Hao Wu, Dept of Computer Science, MU
Title: MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams.
In this talk, I will discuss my most recent research on integrated Formal Methods and Model Driven Engineering. In particular, I will show detailed algorithms and implementation about finding constraint conflicts for inconsistent UML class diagrams. This includes formally presenting a reduction from the set cover problem to boolean satisfiability (SAT/SMT) problem which can be efficiently solved by state-of-the-art SMT solvers. Therefore, people who are generally interested in software engineering/programming languages and algorithms (constraint solving) are particularly welcome. This research will be presented at the International Conference on integrated Formal Methods 2017.
Speaker: Ms Marie Farrell, Dept of Computer Science, MU
Title: Specification Clones: An empirical study of the structure of Event-B specifications
In this talk, I will present an empirical study of formal specifications written in the Event-B language. Our study is exploratory, since it is the first study of its kind, and we formulate metrics for Event-B specifications which quantify the diversity of such specifications in practice. We pay particular attention to refinement as this is one of the most notable features of Event-B. However, Event-B is less well-equipped with other standardised modularisation constructs, and we investigate the impact of this by detecting and analysing specification clones at different levels. We describe our algorithm used to identify clones at the machine, context and event level, and present results from an analysis of a large corpus of Event-B specifications. Our study contributes to furthering research into the area of metrics and modularisation in Event-B. This research will be presented at the International Conference on Software Engineering and Formal Methods 2017.