Synthesising call sequences from OCL operational contracts
Hao Shu Wu · 2019
The Unified Modeling Language (UML) is widely used by software engineers in different phases of software development cycle. It allows them to visualise and depict a system into different diagrams. Among these diagrams, UML class diagrams are used to capture the structure of a system including classes, attributes and associations. The set of operation calls defined in a UML class diagram then capture the behaviour of a system. These operation calls typically constrain the inputs and outputs via a set of pre or postconditions (operational contracts) written in Object Constraint Language (OCL). Hence, a sequence of operation calls conforming to pre or postconditions is crucial to analyse, verify and understand the behaviour of a system. In this paper, we propose a new technique for synthesising call sequences from a set of operational contracts. This technique works by reducing a synthesis problem to a satisfiability modulo theories (SMT) problem. The preliminary results show that our technique is capable of synthesising call sequences at a large scale.