research-article

Timed-rebeca schedulability and deadlock-freedom analysis using floating-time transition system

Authors:

Ehsan Khamespanah,

Zeynab Sabahi Kaviani,

Ramtin Khosravi,

Marjan Sirjani,

Mohammad-Javad IzadiAuthors Info & Claims

AGERE! 2012: Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions

Pages 23 - 34

https://doi.org/10.1145/2414639.2414645

Published: 21 October 2012 Publication History

Abstract

"Timed-Rebeca" is an actor-based modeling language for modeling real-time reactive systems. Its high-level constructs make it more suitable for using it by software practitioners compared to timed-automata based alternatives. Currently, the verification of Timed-Rebeca models is done by converting into timed-automata and using UPPAAL toolset to analyze the model. However, state space explosion and time consumption are the major limitations of using the back-end timed automata model for verification. In this paper, we propose a new approach for direct schedulability checking and deadlock freedom verification of Timed-Rebeca models. The new approach exploits the key feature of Timed-Rebeca, which is encapsulation of concurrent elements. In the proposed method, each state stores the local time of each actor separately, avoiding the need for a global time in the state. This significantly decreases the size of the state space. We prove the bisimilarity of the generated transition system (called floating-time transition system) and the state space generated based on Timed-Rebeca semantics. Also, we provide experimental results showing that the new approach mitigates the state space explosion problem of the former method and allows model-checking of larger problems.

References

[1]

Rebeca Home Page. http://www.rebeca-lang.org.

[2]

Norman Abramson. THE ALOHA SYSTEM: another alternative for computer communications. In AFIPS'70 (Fall): Proceedings of the November 17--19, 1970, fall joint computer conference, pages 281--285, New York, NY, USA, 1970. ACM.

Digital Library

[3]

Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, Arni Hermann Reynisson, Steinar Hugi Sigurdarson, and Marjan Sirjani. Modelling and simulation of asynchronous real-time systems using timed rebeca. In Mohammad Reza Mousavi and António Ravara, editors, FOCLASA, volume 58 of EPTCS, pages 1--19, 2011.

[4]

G. Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, USA, 1990.

Digital Library

[5]

Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183--235, 1994.

Digital Library

[6]

Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.

Digital Library

[7]

Johan Bengtsson, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal - a tool suite for automatic verification of real-time systems. In Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag, editors, Hybrid Systems, volume 1066 of Lecture Notes in Computer Science, pages 232--243. Springer, 1995.

Digital Library

[8]

Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transaction on Programming Languages and Systems, 8(2):244--263, 1986.

Digital Library

[9]

Frank S. de Boer, Tom Chothia, and Mohammad Mahdi Jaghoori. Modular schedulability analysis of concurrent objects in creol. In Farhad Arbab and Marjan Sirjani, editors, FSEN, volume 5961 of Lecture Notes in Computer Science, pages 212--227. Springer, 2009.

Digital Library

[10]

C. Hewitt. Description and theoretical analysis (using schemata) of PLANNER: A language for proving theorems and manipulating models in a robot. MIT Artificial Intelligence Technical Report 258, Department of Computer Science, MIT, April 1972.

[11]

Carl Hewitt. What is commitment? physical, organizational, and social (revised). In Proceedings of Coordination, Organizations, Institutions, and Norms in Agent Systems II, Lecture Notes in Computer Science, pages 293--307. Springer, 2007.

Digital Library

[12]

Carl Hewitt, Peter Bishop, and Richard Steiger. A universal modular actor formalism for artificial intelligence. In Nils J. Nilsson, editor, IJCAI, pages 235--245. William Kaufmann, 1973.

Digital Library

[13]

Mohammad-Javad Izadi. An actor based model for modeling and verification of real-time systems. Master's thesis, University of Tehran, School of Electrical and Computer Engineering, Iran, 2010.

[14]

Mohammad Mahdi Jaghoori, Ali Movaghar, and Marjan Sirjani. Modere: The model-checking engine of Rebeca. In Hisham Haddad, editor, SAC, pages 1810--1815. ACM, 2006.

Digital Library

[15]

Mohammad Mahdi Jaghoori, Marjan Sirjani, Mohammad Reza Mousavi, Ehsan Khamespanah, and Ali Movaghar. Symmetry and partial order reduction techniques in model checking Rebeca. Acta Informatica, 47(1):33--66, 2010.

Digital Library

[16]

M. M. Jaghouri. Time At Your Service: Schedulability Analysis Of Real-Time And Distributed Services. PhD thesis, LIACS, December 2010.

[17]

Dilsun Kirli Kaynar, Nancy A. Lynch, Roberto Segala, and Frits W. Vaandrager. Timed i/o automata: A mathematical framework for modeling and analyzing real-time systems. In RTSS, pages 166--177. IEEE Computer Society, 2003.

Digital Library

[18]

Dilsun Kirli Kaynar, Nancy A. Lynch, Roberto Segala, and Frits W. Vaandrager. The Theory of Timed I/O Automata, Second Edition. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2010.

[19]

Peter Csaba Ölveczky and José Meseguer. Specification of real-time and hybrid systems in rewriting logic. Theor. Comput. Sci., 285(2):359--405, 2002.

Digital Library

[20]

Shangping Ren and Gul Agha. Rtsynchronizer: Language support for real-time specifications in distributed systems. In Richard Gerber and Thomas J. Marlowe, editors, Workshop on Languages, Compilers, & Tools for Real-Time Systems, pages 50--59. ACM, 1995.

Digital Library

[21]

Hamideh Sabouri and Marjan Sirjani. Slicing-based reductions for Rebeca. In Proceedings of FACS 2008. ENTCS, 2008.

[22]

Marjan Sirjani, Frank S. de Boer, and Ali Movaghar-Rahimabadi. Modular verification of a component-based actor language. J. UCS, 11(10):1695--1717, 2005.

[23]

Marjan Sirjani, Ali Movaghar, Amin Shali, and Frank S. de Boer. Modeling and verification of reactive systems using Rebeca. Fundam. Inform., 63(4):385--410, 2004.

Digital Library

[24]

Marjan Sirjani, Amin Shali, Mohammad Mahdi Jaghoori, Hamed Iravanchi, and Ali Movaghar. A front-end tool for automated abstraction and modular verification of actor-based models. In ACSD, pages 145--150. IEEE Computer Society, 2004.

Digital Library

Cited By

Sharifi ZKhosravi RSirjani MKhamespanah E(2020)Towards Formal Analysis of Vehicle Platoons Using Actor Model2020 25th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)10.1109/ETFA46521.2020.9211888(1820-1827)Online publication date: Sep-2020
https://doi.org/10.1109/ETFA46521.2020.9211888
Dehnavi SSedaghatbaf ASalmani BSirjani MKargahi MKhamespanah E(2019)Towards an Actor-based Approach to Design Verified ROS-based Robotic Programs using RebecaProcedia Computer Science10.1016/j.procs.2019.08.012155(59-68)Online publication date: 2019
https://doi.org/10.1016/j.procs.2019.08.012
Sirjani MKhamespanah E(2016)On Time ActorsEssays Dedicated to Frank de Boer on Theory and Practice of Formal Methods - Volume 966010.1007/978-3-319-30734-3_25(373-392)Online publication date: 1-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-319-30734-3_25
Show More Cited By

Index Terms

Timed-rebeca schedulability and deadlock-freedom analysis using floating-time transition system
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition system

Timed Rebeca is an extension of the actor-based modeling language Rebeca that supports timing features. Rebeca is purely actor-based with no shared variables and asynchronous message passing with no explicit receive. Both computation time and network ...
Event-Based Analysis of Timed Rebeca Models using SQL
AGERE! '14: Proceedings of the 4th International Workshop on Programming based on Actors Agents & Decentralized Control

In this paper, we present a simulation-based approach for analysis of Timed Rebeca models to tackle the state space explosion problem. We present a simulation toolkit, TRSim, which uses McErlang as a back-end simulator and stores the occurrences of ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

AGERE! 2012: Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions

October 2012

150 pages

ISBN:9781450316309

DOI:10.1145/2414639

General Chair:
Gul Agha
University of Illinois at Urbana-Champaign, USA
,
Program Chairs:
Rafael H. Bordini
FACIN-PUCRS, Brazil
,
Assaf Marron
Weizmann Institute of Science, Israel
,
Alessandro Ricci
University of Bologna, Italy

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 October 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '12

Sponsor:

SIGPLAN

SPLASH '12: Conference on Systems, Programming, and Applications: Software for Humanity

October 21 - 22, 2012

Arizona, Tucson, USA

Acceptance Rates

Overall Acceptance Rate 19 of 35 submissions, 54%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
109
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sharifi ZKhosravi RSirjani MKhamespanah E(2020)Towards Formal Analysis of Vehicle Platoons Using Actor Model2020 25th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)10.1109/ETFA46521.2020.9211888(1820-1827)Online publication date: Sep-2020
https://doi.org/10.1109/ETFA46521.2020.9211888
Dehnavi SSedaghatbaf ASalmani BSirjani MKargahi MKhamespanah E(2019)Towards an Actor-based Approach to Design Verified ROS-based Robotic Programs using RebecaProcedia Computer Science10.1016/j.procs.2019.08.012155(59-68)Online publication date: 2019
https://doi.org/10.1016/j.procs.2019.08.012
Sirjani MKhamespanah E(2016)On Time ActorsEssays Dedicated to Frank de Boer on Theory and Practice of Formal Methods - Volume 966010.1007/978-3-319-30734-3_25(373-392)Online publication date: 1-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-319-30734-3_25
Khamespanah ESirjani MSabahi Kaviani ZKhosravi RIzadi M(2015)Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition systemScience of Computer Programming10.1016/j.scico.2014.07.00598:P2(184-204)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.07.005
Khamespanah EKhosravi RSirjani MBoix EHaller PRicci AVarela C(2014)Efficient TCTL Model Checking Algorithm for Timed ActorsProceedings of the 4th International Workshop on Programming based on Actors Agents & Decentralized Control10.1145/2687357.2687366(55-66)Online publication date: 20-Oct-2014
https://dl.acm.org/doi/10.1145/2687357.2687366
Magnusson BKhamespanah EKhosravi RSirjani MBoix EHaller PRicci AVarela C(2014)Event-Based Analysis of Timed Rebeca Models using SQLProceedings of the 4th International Workshop on Programming based on Actors Agents & Decentralized Control10.1145/2687357.2687365(43-54)Online publication date: 20-Oct-2014
https://dl.acm.org/doi/10.1145/2687357.2687365
Sabahi-Kaviani ZKhosravi RSirjani MÖlveczky PKhamespanah E(2014)Formal Semantics and Analysis of Timed Rebeca in Real-Time MaudeFormal Techniques for Safety-Critical Systems10.1007/978-3-319-05416-2_12(178-194)Online publication date: 6-Apr-2014
https://doi.org/10.1007/978-3-319-05416-2_12
Kristinsson HJafari AKhamespanah EMagnusson BSirjani MJamali NRicci AWeiss GYonezawa A(2013)Analysing timed Rebeca using McErlangProceedings of the 2013 workshop on Programming based on actors, agents, and decentralized control10.1145/2541329.2541335(25-36)Online publication date: 27-Oct-2013
https://dl.acm.org/doi/10.1145/2541329.2541335

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten