Modeling two way concurrent buffer system using timed automata in UPPAAL

Rohit Mishra, Md Zeeshaan, Sanjay Singh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Two way buffer system is a system that exhibits transfer of data using two buffers concurrently. It includes processes that synchronize to exchange data with each other along with executing certain delays between these synchronizations. In existing Tiny two way buffer system, both generators produce packets in half duplex manner after a delay of 10 seconds. However, generator one has an initial shift of 5 seconds after which it begins sending a packet every 10 seconds. Hence, initial delay for generator one is 15 seconds and for generator two it is 10 seconds. Due to this initial shift, both generators produce packets alternatively and is deadlock free as the packets do not meet at the same time instant. Moreover, the existing system model is not concurrent and hence takes more time for packet transfer in every iteration. In this paper we have proposed a model of buffer system using an additional dummy buffer for transfer of data packets, by introducing delay in various buffers of the proposed system that speeds up the transfer of packets. As a result the transfer of data becomes concurrent, deadlock free and hence the model proposed is time efficient. To model and simulate the proposed system we have used UPPAAL as a model checking tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata. Simulation results shows that the proposed two way buffer system is fully concurrent and time efficient as compared to the existing buffer system.

Original languageEnglish
Title of host publicationProceedings of the 2012 World Congress on Information and Communication Technologies, WICT 2012
Pages846-851
Number of pages6
DOIs
Publication statusPublished - 01-12-2012
Event2012 World Congress on Information and Communication Technologies, WICT 2012 - Trivandrum, India
Duration: 30-10-201202-11-2012

Conference

Conference2012 World Congress on Information and Communication Technologies, WICT 2012
CountryIndia
CityTrivandrum
Period30-10-1202-11-12

Fingerprint

Model checking
Electronic data interchange
Real time systems
Synchronization

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Information Systems

Cite this

Mishra, R., Zeeshaan, M., & Singh, S. (2012). Modeling two way concurrent buffer system using timed automata in UPPAAL. In Proceedings of the 2012 World Congress on Information and Communication Technologies, WICT 2012 (pp. 846-851). [6409193] https://doi.org/10.1109/WICT.2012.6409193
Mishra, Rohit ; Zeeshaan, Md ; Singh, Sanjay. / Modeling two way concurrent buffer system using timed automata in UPPAAL. Proceedings of the 2012 World Congress on Information and Communication Technologies, WICT 2012. 2012. pp. 846-851
@inproceedings{93fb095410584f7e9d5d3f9a97032f36,
title = "Modeling two way concurrent buffer system using timed automata in UPPAAL",
abstract = "Two way buffer system is a system that exhibits transfer of data using two buffers concurrently. It includes processes that synchronize to exchange data with each other along with executing certain delays between these synchronizations. In existing Tiny two way buffer system, both generators produce packets in half duplex manner after a delay of 10 seconds. However, generator one has an initial shift of 5 seconds after which it begins sending a packet every 10 seconds. Hence, initial delay for generator one is 15 seconds and for generator two it is 10 seconds. Due to this initial shift, both generators produce packets alternatively and is deadlock free as the packets do not meet at the same time instant. Moreover, the existing system model is not concurrent and hence takes more time for packet transfer in every iteration. In this paper we have proposed a model of buffer system using an additional dummy buffer for transfer of data packets, by introducing delay in various buffers of the proposed system that speeds up the transfer of packets. As a result the transfer of data becomes concurrent, deadlock free and hence the model proposed is time efficient. To model and simulate the proposed system we have used UPPAAL as a model checking tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata. Simulation results shows that the proposed two way buffer system is fully concurrent and time efficient as compared to the existing buffer system.",
author = "Rohit Mishra and Md Zeeshaan and Sanjay Singh",
year = "2012",
month = "12",
day = "1",
doi = "10.1109/WICT.2012.6409193",
language = "English",
isbn = "9781467348041",
pages = "846--851",
booktitle = "Proceedings of the 2012 World Congress on Information and Communication Technologies, WICT 2012",

}

Mishra, R, Zeeshaan, M & Singh, S 2012, Modeling two way concurrent buffer system using timed automata in UPPAAL. in Proceedings of the 2012 World Congress on Information and Communication Technologies, WICT 2012., 6409193, pp. 846-851, 2012 World Congress on Information and Communication Technologies, WICT 2012, Trivandrum, India, 30-10-12. https://doi.org/10.1109/WICT.2012.6409193

Modeling two way concurrent buffer system using timed automata in UPPAAL. / Mishra, Rohit; Zeeshaan, Md; Singh, Sanjay.

Proceedings of the 2012 World Congress on Information and Communication Technologies, WICT 2012. 2012. p. 846-851 6409193.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Modeling two way concurrent buffer system using timed automata in UPPAAL

AU - Mishra, Rohit

AU - Zeeshaan, Md

AU - Singh, Sanjay

PY - 2012/12/1

Y1 - 2012/12/1

N2 - Two way buffer system is a system that exhibits transfer of data using two buffers concurrently. It includes processes that synchronize to exchange data with each other along with executing certain delays between these synchronizations. In existing Tiny two way buffer system, both generators produce packets in half duplex manner after a delay of 10 seconds. However, generator one has an initial shift of 5 seconds after which it begins sending a packet every 10 seconds. Hence, initial delay for generator one is 15 seconds and for generator two it is 10 seconds. Due to this initial shift, both generators produce packets alternatively and is deadlock free as the packets do not meet at the same time instant. Moreover, the existing system model is not concurrent and hence takes more time for packet transfer in every iteration. In this paper we have proposed a model of buffer system using an additional dummy buffer for transfer of data packets, by introducing delay in various buffers of the proposed system that speeds up the transfer of packets. As a result the transfer of data becomes concurrent, deadlock free and hence the model proposed is time efficient. To model and simulate the proposed system we have used UPPAAL as a model checking tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata. Simulation results shows that the proposed two way buffer system is fully concurrent and time efficient as compared to the existing buffer system.

AB - Two way buffer system is a system that exhibits transfer of data using two buffers concurrently. It includes processes that synchronize to exchange data with each other along with executing certain delays between these synchronizations. In existing Tiny two way buffer system, both generators produce packets in half duplex manner after a delay of 10 seconds. However, generator one has an initial shift of 5 seconds after which it begins sending a packet every 10 seconds. Hence, initial delay for generator one is 15 seconds and for generator two it is 10 seconds. Due to this initial shift, both generators produce packets alternatively and is deadlock free as the packets do not meet at the same time instant. Moreover, the existing system model is not concurrent and hence takes more time for packet transfer in every iteration. In this paper we have proposed a model of buffer system using an additional dummy buffer for transfer of data packets, by introducing delay in various buffers of the proposed system that speeds up the transfer of packets. As a result the transfer of data becomes concurrent, deadlock free and hence the model proposed is time efficient. To model and simulate the proposed system we have used UPPAAL as a model checking tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata. Simulation results shows that the proposed two way buffer system is fully concurrent and time efficient as compared to the existing buffer system.

UR - http://www.scopus.com/inward/record.url?scp=84873360461&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84873360461&partnerID=8YFLogxK

U2 - 10.1109/WICT.2012.6409193

DO - 10.1109/WICT.2012.6409193

M3 - Conference contribution

AN - SCOPUS:84873360461

SN - 9781467348041

SP - 846

EP - 851

BT - Proceedings of the 2012 World Congress on Information and Communication Technologies, WICT 2012

ER -

Mishra R, Zeeshaan M, Singh S. Modeling two way concurrent buffer system using timed automata in UPPAAL. In Proceedings of the 2012 World Congress on Information and Communication Technologies, WICT 2012. 2012. p. 846-851. 6409193 https://doi.org/10.1109/WICT.2012.6409193