Transformation of PROMELA to Channel Systems
| Main Authors: | Huda, Sheila Nurul, Pulungan, Reza |
|---|---|
| Format: | Proceeding PeerReviewed application/pdf |
| Bahasa: | eng |
| Terbitan: |
, 2013
|
| Subjects: | |
| Online Access: |
https://repository.ugm.ac.id/35109/1/HP-CSIT-13.pdf https://repository.ugm.ac.id/35109/ |
| ctrlnum |
35109 |
|---|---|
| fullrecord |
<?xml version="1.0"?>
<dc schemaLocation="http://www.openarchives.org/OAI/2.0/oai_dc/ http://www.openarchives.org/OAI/2.0/oai_dc.xsd"><relation>https://repository.ugm.ac.id/35109/</relation><title>Transformation of PROMELA to Channel Systems</title><creator>Huda, Sheila Nurul</creator><creator>Pulungan, Reza</creator><subject>Computation Theory and Mathematics</subject><description>This paper reports on an implementation of transformation of PROMELA models into Channel Systems, which will be further transformed into Labeled Transition Systems (LTSs). The objective of this transformation is to obtain a formal semantics for further model checking purposes. A Channel System is a way to describe communicating processes that run in parallel, where each process is represented by a Program Graph (PG). The main part of a Program Graph is a location transition which consists of the initial location, a guard which determines whether the transition is executable or not, an action that will be executed in the location transition, and the next location. This paper defined the location transition for PROMELA constructs such as assignments, communication actions, if-fi, do-od, and atomic steps.</description><date>2013-06-18</date><type>Journal:Proceeding</type><type>PeerReview:PeerReviewed</type><type>File:application/pdf</type><language>eng</language><identifier>https://repository.ugm.ac.id/35109/1/HP-CSIT-13.pdf</identifier><identifier> Huda, Sheila Nurul and Pulungan, Reza (2013) Transformation of PROMELA to Channel Systems. In: The 2013 International Conference on Computer Science and Information Technology (CSIT-2013), June 16-18, 2013, Yogyakarta. </identifier><recordID>35109</recordID></dc>
|
| language |
eng |
| format |
Journal:Proceeding Journal PeerReview:PeerReviewed PeerReview File:application/pdf File |
| author |
Huda, Sheila Nurul Pulungan, Reza |
| title |
Transformation of PROMELA to Channel Systems |
| publishDate |
2013 |
| topic |
Computation Theory and Mathematics |
| url |
https://repository.ugm.ac.id/35109/1/HP-CSIT-13.pdf https://repository.ugm.ac.id/35109/ |
| contents |
This paper reports on an implementation of transformation of PROMELA models into Channel Systems, which will be further transformed into Labeled Transition Systems (LTSs). The objective of this transformation is to obtain a formal semantics for further model checking purposes. A Channel System is a way to describe communicating processes that run in parallel, where each process is represented by a Program Graph (PG). The main part of a Program Graph is a location transition which consists of the initial location, a guard which determines whether the transition is executable or not, an action that will be executed in the location transition, and the next location. This paper defined the location transition for PROMELA constructs such as assignments, communication actions, if-fi, do-od, and atomic steps. |
| id |
IOS2744.35109 |
| institution |
Universitas Gadjah Mada |
| institution_id |
19 |
| institution_type |
library:university library |
| library |
Perpustakaan Pusat Universitas Gadjah Mada |
| library_id |
488 |
| collection |
UGM Repository |
| repository_id |
2744 |
| subject_area |
Karya Umum |
| city |
SLEMAN |
| province |
DAERAH ISTIMEWA YOGYAKARTA |
| repoId |
IOS2744 |
| first_indexed |
2016-09-14T18:09:55Z |
| last_indexed |
2016-09-22T21:23:19Z |
| recordtype |
dc |
| _version_ |
1765815495917830144 |
| score |
17.538404 |