A formal semantics of timed activity diagrams and its PROMELA translation

Nicolas Guelfi; Amel Mammar

doi:10.1109/APSEC.2005.7

A formal semantics of timed activity diagrams and its PROMELA translation

Nicolas Guelfi, Amel Mammar

University of Luxembourg

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

The lack of a precise semantics for UML activity diagrams makes the reasoning on models constructed using such diagrams infeasible. However, such diagrams are widely used in domains that require a certain degree of confidence. Due to economical interests, the business domain is one of these. To enhance confidence level of UML activity diagrams, this paper provides a formal definition of their syntax and semantics. The main interest of our approach is that we chose UML activity diagrams, which are recognized to be more tractable by engineers, and we extend them with timing constraints. We outline the translation of our semantics into the PROMELA input language of the SPIN model checker which can be used to check several properties.

Original language	English
Title of host publication	Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05
Pages	283-290
Number of pages	8
DOIs	https://doi.org/10.1109/APSEC.2005.7
Publication status	Published - 1 Dec 2005
Externally published	Yes
Event	12th Asia-Pacific Software Engineering Conference, APSEC'05 - Taipei, Taiwan, Province of China Duration: 15 Dec 2005 → 17 Dec 2005

Publication series

Name	Proceedings - Asia-Pacific Software Engineering Conference, APSEC
Volume	2005
ISSN (Print)	1530-1362

Conference

Conference	12th Asia-Pacific Software Engineering Conference, APSEC'05
Country/Territory	Taiwan, Province of China
City	Taipei
Period	15/12/05 → 17/12/05

Access to Document

10.1109/APSEC.2005.7

Cite this

@inproceedings{095ea64d34e44dc6bc91cea7aba81393,

title = "A formal semantics of timed activity diagrams and its PROMELA translation",

abstract = "The lack of a precise semantics for UML activity diagrams makes the reasoning on models constructed using such diagrams infeasible. However, such diagrams are widely used in domains that require a certain degree of confidence. Due to economical interests, the business domain is one of these. To enhance confidence level of UML activity diagrams, this paper provides a formal definition of their syntax and semantics. The main interest of our approach is that we chose UML activity diagrams, which are recognized to be more tractable by engineers, and we extend them with timing constraints. We outline the translation of our semantics into the PROMELA input language of the SPIN model checker which can be used to check several properties.",

author = "Nicolas Guelfi and Amel Mammar",

year = "2005",

month = dec,

day = "1",

doi = "10.1109/APSEC.2005.7",

language = "English",

isbn = "0769524656",

series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",

pages = "283--290",

booktitle = "Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05",

note = "12th Asia-Pacific Software Engineering Conference, APSEC'05 ; Conference date: 15-12-2005 Through 17-12-2005",

}

Guelfi, N & Mammar, A 2005, A formal semantics of timed activity diagrams and its PROMELA translation. in Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05., 1607163, Proceedings - Asia-Pacific Software Engineering Conference, APSEC, vol. 2005, pp. 283-290, 12th Asia-Pacific Software Engineering Conference, APSEC'05, Taipei, Taiwan, Province of China, 15/12/05. https://doi.org/10.1109/APSEC.2005.7

A formal semantics of timed activity diagrams and its PROMELA translation. / Guelfi, Nicolas; Mammar, Amel.
Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05. 2005. p. 283-290 1607163 (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; Vol. 2005).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A formal semantics of timed activity diagrams and its PROMELA translation

AU - Guelfi, Nicolas

AU - Mammar, Amel

PY - 2005/12/1

Y1 - 2005/12/1

N2 - The lack of a precise semantics for UML activity diagrams makes the reasoning on models constructed using such diagrams infeasible. However, such diagrams are widely used in domains that require a certain degree of confidence. Due to economical interests, the business domain is one of these. To enhance confidence level of UML activity diagrams, this paper provides a formal definition of their syntax and semantics. The main interest of our approach is that we chose UML activity diagrams, which are recognized to be more tractable by engineers, and we extend them with timing constraints. We outline the translation of our semantics into the PROMELA input language of the SPIN model checker which can be used to check several properties.

AB - The lack of a precise semantics for UML activity diagrams makes the reasoning on models constructed using such diagrams infeasible. However, such diagrams are widely used in domains that require a certain degree of confidence. Due to economical interests, the business domain is one of these. To enhance confidence level of UML activity diagrams, this paper provides a formal definition of their syntax and semantics. The main interest of our approach is that we chose UML activity diagrams, which are recognized to be more tractable by engineers, and we extend them with timing constraints. We outline the translation of our semantics into the PROMELA input language of the SPIN model checker which can be used to check several properties.

U2 - 10.1109/APSEC.2005.7

DO - 10.1109/APSEC.2005.7

M3 - Conference contribution

AN - SCOPUS:33847255927

SN - 0769524656

SN - 9780769524658

T3 - Proceedings - Asia-Pacific Software Engineering Conference, APSEC

SP - 283

EP - 290

BT - Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05

T2 - 12th Asia-Pacific Software Engineering Conference, APSEC'05

Y2 - 15 December 2005 through 17 December 2005

ER -

A formal semantics of timed activity diagrams and its PROMELA translation

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this