Analyzing Behavioral Aspects of UML Design Class Models against Temporal Properties

Class models play central roles in model-driven development (MDD). Automated analysis of class models is crucial to uncover design problems. In previous work, we described a rigorous lightweight approach to analyzing operation specifications in UML design class models against temporal properties. However, the approach lacks a mechanism to handle the analysis of large class models. This paper presents a slicing algorithm that can be used to scale the analysis to large class models. We performed a preliminary evaluation using the Steam Boiler Control System. The results are presented in this paper.