A Framework for An LTS Semantics for PROMELA
A high-level specification language PROMELA can be used not only to model interactions that occur in distributed or reactive systems, but also to express requirements of logical correctness about those interactions. Several approaches to a formal semantics for PROMELA have been presented, ranging fr...
Saved in:
Main Authors: | , |
---|---|
Format: | Conference or Workshop Item PeerReviewed |
Language: | English |
Published: |
2011
|
Subjects: | |
Online Access: | https://repository.ugm.ac.id/35114/1/SP-SEAMS-11.pdf https://repository.ugm.ac.id/35114/ |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Universitas Gadjah Mada |
Language: | English |
id |
id-ugm-repo.35114 |
---|---|
record_format |
dspace |
spelling |
id-ugm-repo.351142014-06-17T22:54:20Z https://repository.ugm.ac.id/35114/ A Framework for An LTS Semantics for PROMELA Suprapto, Suprapto Pulungan, Reza Makalah prosiding A high-level specification language PROMELA can be used not only to model interactions that occur in distributed or reactive systems, but also to express requirements of logical correctness about those interactions. Several approaches to a formal semantics for PROMELA have been presented, ranging from the less complete formal semantics to the more complete ones. This paper presents a significantly different approach to provide a formal semantics for PROMELA model, namely by an operational semantics given as a set of Structured Operational Semantics (SOS) rules. The operational semantics of a PROMELA statement with variables and channels is given by a program graph. The program graphs for the processes of a PROMELA model constitute a channel system. Finally, the transition system semantics for channel systems yields a transition system that formalizes the stepwise behavior of the PROMELA model. 2011-07-15 Conference or Workshop Item PeerReviewed application/pdf en https://repository.ugm.ac.id/35114/1/SP-SEAMS-11.pdf Suprapto, Suprapto and Pulungan, Reza (2011) A Framework for An LTS Semantics for PROMELA. In: The 6th South East Asian Mathematical Society-Gadjah Mada University (SEAMS-GMU) 2011 International Conference on Mathematics and Its Applications, July 12-15, 2011, Yogyakarta. |
institution |
Universitas Gadjah Mada |
building |
UGM Library |
country |
Indonesia |
collection |
Repository Civitas UGM |
language |
English |
topic |
Makalah prosiding |
spellingShingle |
Makalah prosiding Suprapto, Suprapto Pulungan, Reza A Framework for An LTS Semantics for PROMELA |
description |
A high-level specification language PROMELA can be used not only to model interactions that occur in distributed or reactive systems, but also to express requirements of logical correctness about those interactions. Several approaches to a formal semantics for PROMELA have been presented, ranging from the less complete formal semantics to the more complete ones. This paper presents a significantly different approach to provide a formal semantics for PROMELA model, namely by an operational semantics given as a set of Structured Operational Semantics (SOS) rules. The operational semantics of a PROMELA statement with variables and channels is given by a program graph. The program graphs for the processes of a PROMELA model constitute a channel system. Finally, the transition system semantics for channel systems yields a transition system that formalizes the stepwise behavior of the PROMELA model. |
format |
Conference or Workshop Item PeerReviewed |
author |
Suprapto, Suprapto Pulungan, Reza |
author_facet |
Suprapto, Suprapto Pulungan, Reza |
author_sort |
Suprapto, Suprapto |
title |
A Framework for An LTS Semantics for PROMELA |
title_short |
A Framework for An LTS Semantics for PROMELA |
title_full |
A Framework for An LTS Semantics for PROMELA |
title_fullStr |
A Framework for An LTS Semantics for PROMELA |
title_full_unstemmed |
A Framework for An LTS Semantics for PROMELA |
title_sort |
framework for an lts semantics for promela |
publishDate |
2011 |
url |
https://repository.ugm.ac.id/35114/1/SP-SEAMS-11.pdf https://repository.ugm.ac.id/35114/ |
_version_ |
1681219450493206528 |