Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus

Vitus S. W. Lam; Julian Padget

doi:10.1007/11589976

Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus

Department of Computer Science

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Abstract

UML 2.0, like UML 1.x, provides only a set of notations for specifying different aspects of a system. The problem of checking consistency between various types of models in software development is still not fully addressed. In this paper, we suggest the use of an algebraic approach for verifying whether consistency between sequence diagrams and statechart diagrams is preserved. First, statechart diagrams are encoded in the pi-calculus. Then, each object in a sequence diagram is translated into its equivalent pi-calculus definitions and verified against the corresponding statechart diagram represented in the pi-calculus using the Mobility Workbench. The applicability of the proposed approach is illustrated with an agent-based payment protocol.

Original language	English
Title of host publication	Integrated Formal Methods
Subtitle of host publication	Proceedings of 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005
Editors	J. M. T. Romijn, G. P. Smith, J. C. van de Pol
Place of Publication	Berlin, Germany
Publisher	Springer
Pages	347-365
Number of pages	19
ISBN (Electronic)	9783540322405
ISBN (Print)	9783540304920
DOIs	https://doi.org/10.1007/11589976
Publication status	Published - 2005

Publication series

Name	Lecture Notes in Computer Science : Programming and Software Engineering
Volume	3771

Bibliographical note

ID number: ISI:000234830600020

Access to Document

10.1007/11589976

http://dx.doi.org/10.1007/11589976

Cite this

Lam, V. S. W., & Padget, J. (2005). Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus. In J. M. T. Romijn, G. P. Smith, & J. C. van de Pol (Eds.), Integrated Formal Methods: Proceedings of 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005 (pp. 347-365). (Lecture Notes in Computer Science : Programming and Software Engineering; Vol. 3771). Springer. https://doi.org/10.1007/11589976

Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus. / Lam, Vitus S. W.; Padget, Julian.
Integrated Formal Methods: Proceedings of 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005. ed. / J. M. T. Romijn; G. P. Smith; J. C. van de Pol. Berlin, Germany: Springer, 2005. p. 347-365 (Lecture Notes in Computer Science : Programming and Software Engineering; Vol. 3771).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Lam, VSW & Padget, J 2005, Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus. in JMT Romijn, GP Smith & JC van de Pol (eds), Integrated Formal Methods: Proceedings of 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005. Lecture Notes in Computer Science : Programming and Software Engineering, vol. 3771, Springer, Berlin, Germany, pp. 347-365. https://doi.org/10.1007/11589976

Lam VSW, Padget J. Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus. In Romijn JMT, Smith GP, van de Pol JC, editors, Integrated Formal Methods: Proceedings of 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005. Berlin, Germany: Springer. 2005. p. 347-365. (Lecture Notes in Computer Science : Programming and Software Engineering). doi: 10.1007/11589976

Lam, Vitus S. W. ; Padget, Julian. / Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus. Integrated Formal Methods: Proceedings of 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005. editor / J. M. T. Romijn ; G. P. Smith ; J. C. van de Pol. Berlin, Germany : Springer, 2005. pp. 347-365 (Lecture Notes in Computer Science : Programming and Software Engineering).

@inproceedings{cf0c1771cbe54244b21041d1df309633,

title = "Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus",

abstract = "UML 2.0, like UML 1.x, provides only a set of notations for specifying different aspects of a system. The problem of checking consistency between various types of models in software development is still not fully addressed. In this paper, we suggest the use of an algebraic approach for verifying whether consistency between sequence diagrams and statechart diagrams is preserved. First, statechart diagrams are encoded in the pi-calculus. Then, each object in a sequence diagram is translated into its equivalent pi-calculus definitions and verified against the corresponding statechart diagram represented in the pi-calculus using the Mobility Workbench. The applicability of the proposed approach is illustrated with an agent-based payment protocol.",

author = "Lam, {Vitus S. W.} and Julian Padget",

note = "ID number: ISI:000234830600020",

year = "2005",

doi = "10.1007/11589976",

language = "English",

isbn = "9783540304920",

series = "Lecture Notes in Computer Science : Programming and Software Engineering",

publisher = "Springer",

pages = "347--365",

editor = "Romijn, {J. M. T.} and Smith, {G. P.} and { van de Pol}, {J. C.}",

booktitle = "Integrated Formal Methods",

}

TY - GEN

T1 - Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus

AU - Lam, Vitus S. W.

AU - Padget, Julian

N1 - ID number: ISI:000234830600020

PY - 2005

Y1 - 2005

N2 - UML 2.0, like UML 1.x, provides only a set of notations for specifying different aspects of a system. The problem of checking consistency between various types of models in software development is still not fully addressed. In this paper, we suggest the use of an algebraic approach for verifying whether consistency between sequence diagrams and statechart diagrams is preserved. First, statechart diagrams are encoded in the pi-calculus. Then, each object in a sequence diagram is translated into its equivalent pi-calculus definitions and verified against the corresponding statechart diagram represented in the pi-calculus using the Mobility Workbench. The applicability of the proposed approach is illustrated with an agent-based payment protocol.

AB - UML 2.0, like UML 1.x, provides only a set of notations for specifying different aspects of a system. The problem of checking consistency between various types of models in software development is still not fully addressed. In this paper, we suggest the use of an algebraic approach for verifying whether consistency between sequence diagrams and statechart diagrams is preserved. First, statechart diagrams are encoded in the pi-calculus. Then, each object in a sequence diagram is translated into its equivalent pi-calculus definitions and verified against the corresponding statechart diagram represented in the pi-calculus using the Mobility Workbench. The applicability of the proposed approach is illustrated with an agent-based payment protocol.

UR - http://dx.doi.org/10.1007/11589976

U2 - 10.1007/11589976

DO - 10.1007/11589976

M3 - Chapter in a published conference proceeding

SN - 9783540304920

T3 - Lecture Notes in Computer Science : Programming and Software Engineering

SP - 347

EP - 365

BT - Integrated Formal Methods

A2 - Romijn, J. M. T.

A2 - Smith, G. P.

A2 - van de Pol, J. C.

PB - Springer

CY - Berlin, Germany

ER -

Consistency checking of sequence diagrams and statechart diagrams using the pi-calculus

Abstract

Publication series

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this