Model checking dynamic UML consistency

被引：0

作者：

Department of Informatics, School of Math., Peking University, Beijing, China ^{[1
]}

不详 ^{[2
]}

机构：

[1] Department of Informatics, School of Math., Peking University, Beijing

来源：

Lect. Notes Comput. Sci. | 2006年 / 440-459期

关键词：

Algorithm; Consistency; Model checking; Semantics; Simulation; UML;

D O I：

10.1007/11901433_24

中图分类号：

学科分类号：

摘要：

UML is widely accepted and extensively used in software modeling. However, using different diagrams to model different aspects of a system brings the risk of inconsistency among diagrams. In this paper, we investigate an approach to check the consistency between the sequence diagrams and statechart diagrams using the SPIN model checker. To deal with the hierarchy structure of statechart diagrams, we propose a formalism called Split Automata, a variant of automata, which is helpful to bridge the statechart diagrams to SPIN efficiently. Compared with the existing work on model checking UML which do not have formal verification for their translation from UML to the model checker, we formally define the semantics and prove that the automatically translated model (i.e. Split Automata) does simulate the UML model. In this way, we can guarantee that the translated model does represent the original model. © Springer-Verlag Berlin Heidelberg 2006.

引用

页码：440 / 459

页数：19

共 17 条

[1]

Astesiano E., Reggio G., An attempt at analysing the consistency problems in the UML from a classical algebraic viewpoint, WADT 2002, LNCS, 2755, (2003)

[2]

Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Sequential circuit verification using symbolic model checking, DAC '90: Proceedings of the 27th ACM/IEEE Conference on Design Automation, pp. 46-51, (1990)

[3]

Clarke E.M., Grumberg O., Peled D.A., Model Checking, (2000)

[4]

Fowler M., What is the point of UML, LNCS, 1618, (1998)

[5]

Kuester J.M., Engels G., Groencwegen L., Consistent interaction of software components, Proc. of IDPT 2002, (2002)

[6]

Gallardo M.M., Merino P., Pimentel E., Debugging UML designs with model checking, Journal of Object Technology, 1, 2, pp. 101-117, (2002)

[7]

He J., Li X., Liu Z., RCOS: A refinement calculus for object-oriented systems, Theoretical Computer Science

[8]

Holzmann G.J., The SPIN Model Checker: Primer and Reference Manual, (2003)

[9]

Inverardi P., Muccini H., Pelliccione P., Checking consistency between architectural models using SPIN, Proc. of STRAW'01, (2001)

[10]

Jacobson I., Rumbaugh J., Booch G., The Unified Modelling Language Reference Manual, (1999)

← 1 2 →