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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05
Pages	283-290
Nombre de pages	8
Les DOIs	https://doi.org/10.1109/APSEC.2005.7
état	Publié - 1 déc. 2005
Modification externe	Oui
Evénement	12th Asia-Pacific Software Engineering Conference, APSEC'05 - Taipei, Taiwan Durée: 15 déc. 2005 → 17 déc. 2005

Série de publications

Nom	Proceedings - Asia-Pacific Software Engineering Conference, APSEC
Volume	2005
ISSN (imprimé)	1530-1362

Une conférence

Une conférence	12th Asia-Pacific Software Engineering Conference, APSEC'05
Pays/Territoire	Taiwan
La ville	Taipei
période	15/12/05 → 17/12/05

Accès au document

10.1109/APSEC.2005.7

Contient cette citation

@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. Dans Proceedings - 12th Asia-Pacific Software Engineering Conference, APSEC'05., 1607163, Proceedings - Asia-Pacific Software Engineering Conference, APSEC, VOL. 2005, p. 283-290, 12th Asia-Pacific Software Engineering Conference, APSEC'05, Taipei, Taiwan, 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation