Building reliable software systems is a complex but important challenge of modern engineering. A fundamental determiner of software reliability is the methodology used to develop and verify both designs and implementations. Current tools have significant limitations that increase the cost and development time of software systems. There is no question that one of the fundamental tasks in computer and information science is advancing the state of our development methods: We need better techniques and tools for developing correct and predictable software systems.
Current methodologies are proved to be insufficient and ineffective in developing reliable and trustworthy distributed and asynchronous systems, specially when we are concerned about timing constraints. So, a main challenge of software engineering in future is to establish novel ideas, methods, and techniques for developing systems of this category. In the ICT (Information and Communication Technologies) work programme of 2010 of the European Commission, the first challenge is pervasive and trustworthy network and service infrastructures. At the same time formal analysis and verification are inevitable techniques to ensure dependability of systems.
In TARO (Timed Asynchronous Reactive Objects in Distributed Systems) project, we aim at contributing to this research effort. We propose to develop a methodology, techniques and tools, for building fully asynchronous systems, whose behaviour depends crucially on timing constraints, with associated formal analysis and verification support. Our methodology is based on proposing an actor-based modeling language, extended with timing constraints and supported by formal verification tools. The research emphasis in the project places it firmly at the core of the grand challenge of developing reliable networked systems, and at the leading edge of research in software engineering. The real-world case studies will be used as testbeds for establishing the applicability of the proposed methodology and of the associated tools. They will tie together the theoretical and practical aspects of the research, resulting in a substantial synergy.
The following case studies are also developed which include TCTL property specifications.
Ehsan Khamespanah, Kirill Mechitov, Marjan Sirjani, Gul Agha: Modeling and Analyzing Real-Time Wireless Sensor and Actuator Networks Using Actors and Model Checking, Submitted to Software Tools for Technology Transfer, 2017 [pdf]
Ehsan Khamespanah, Ramtin Khosravi, Marjan Sirjani: An Efficient TCTL Model Checking Algorithm and A Reduction Technique for Verification of Timed Actor Models, Submitted to Science of Computer Programming, 2017 [pdf]
Marjan Sirjani, Ehsan Khamespanah, Kirill Mechitov, Gul Agha: A Compositional Approach for Modeling and Timing Analysis of Wireless Sensor and Actuator Networks, CRTS, 2016 [pdf]
Ehsan Khamespanah, Kirill Mechitov, Marjan Sirjani, Gul Agha: Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking, SPIN, 2016 [pdf] [bib]
Marjan Sirjani, Ehsan Khamespanah: On Time Actors, LNCS 9660, 2016 [pdf] [bib]
Ehsan Khamespanah, Marjan Sirjani, Zeynab Sabahi Kaviani, Ramtin Khosravi, Mohammad-Javad Izadi: Timed Rebeca Schedulability and Deadlock Freedom Analysis Using Bounded Floating Time Transition System, Science of Computer Programming, 2015 [pdf] [bib]
Ehsan Khamespanah, Marjan Sirjani, Mahesh Viswanathan, Ramtin Khosravi: Floating Time Transition System: More Efficient Analysis of Timed Actors, FACS, 2015 [pdf] [bib]
Arni Hermann Reynisson, Marjan Sirjani, Luca Aceto, Matteo Cimini, Ali Jafari, Anna Ingolfsdottir, Steinar Hugi Sigurdarson, Modelling and simulation of asynchronous real-time systems using Timed Rebeca, Science of Computer Programming, 2014 [pdf] [bib]
Brynjar Magnusson, Ehsan Khamespanah, Marjan Sirjani, Ramtin Khosravi, Event-based Analysis of Timed Rebeca Models using SQL, AGERE 2014, USA, October 2014 [pdf] [bib]
Ehsan Khamespanah, Marjan Sirjani, Ramtin Khosravi, Efficient TCTL Model Checking Algorithm for Timed Actors, AGERE 2014, USA, October 2014 [pdf] [bib]
Haukur Kristinsson: Event-Based analysis of Read-Time Actor Models - Master Thesis, Reykjavík University, Iceland (2012) [pdf]
Brynjar Magnusson: Simulation-Based Analysis of Timed Rebeca Using TeProp and SQL - Master Thesis, Reykjavík University, Iceland (2012) [pdf]
Ehsan Khamespanah, Zeynab Sabahi Kaviani, Ramtin Khosravi, Marjan Sirjani, Mohammad-Javad Izadi: Timed-Rebeca Schedulability and Deadlock-Freedom Analysis Using Floating-Time Transition System, AGERE, 2012 [pdf] [bib]
Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, Arni Hermann Reynisson, Steinar Hugi Sigurdarson, Marjan Sirjani: Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca FOCLASA, 2011 [pdf] [bib]
Arni Hermann Reynisson: Timed Rebeca Refinement and Simulation - Master Thesis, Reykjavík University, Iceland (2011) [pdf]