mdh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Sirjani, Marjan
Publications (10 of 16) Show all publications
Jahandideh, I., Ghassemi, F. & Sirjani, M. (2019). Hybrid rebeca: Modeling and analyzing of cyber-physical systems. In: Lect. Notes Comput. Sci.: . Paper presented at CyPhy 2018, WESE 2018 (pp. 3-27). Springer Verlag
Open this publication in new window or tab >>Hybrid rebeca: Modeling and analyzing of cyber-physical systems
2019 (English)In: Lect. Notes Comput. Sci., Springer Verlag , 2019, p. 3-27Conference paper, Published paper (Refereed)
Abstract [en]

In cyber-physical systems like automotive systems, there are components like sensors, actuators, and controllers that communicate asynchronously with each other. The computational model of actor supports modeling distributed asynchronously communicating systems. We propose Hybrid Rebeca language to support modeling of cyber-physical systems. Hybrid Rebeca is an extension of actor-based language Rebeca. In this extension, physical actors are introduced as new computational entities to encapsulate physical behaviors. To support various means of communication among the entities, the network is explicitly modeled as a separate entity from actors. We derive hybrid automata as the basis for analysis of Hybrid Rebeca models. We demonstrate the applicability of our approach through a case study in the domain of automotive systems. We use SpaceEx framework for the analysis of the case study. 

Place, publisher, year, edition, pages
Springer Verlag, 2019
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 11615 LNCS
Keywords
Actor model, Cyber-physical systems, Hybrid automata
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-44935 (URN)10.1007/978-3-030-23703-5_1 (DOI)2-s2.0-85069162822 (Scopus ID)9783030237028 (ISBN)
Conference
CyPhy 2018, WESE 2018
Note

Export Date: 1 August 2019; Conference Paper; Correspondence Address: Ghassemi, F.; School of Electrical and Computer Engineering, University of TehranIran; email: fghassemi@ut.ac.ir

Available from: 2019-08-01 Created: 2019-08-01 Last updated: 2019-08-01Bibliographically approved
Lohstroh, M., Schoeberl, M., Goens, A., Wasicek, A., Gill, C., Sirjani, M. & Lee, E. A. (2019). Invited: Actors revisited for time-critical systems. In: Proceedings - Design Automation Conference: . Paper presented at 56th Annual Design Automation Conference, DAC 2019, 2 June 2019 through 6 June 2019. Institute of Electrical and Electronics Engineers Inc.
Open this publication in new window or tab >>Invited: Actors revisited for time-critical systems
Show others...
2019 (English)In: Proceedings - Design Automation Conference, Institute of Electrical and Electronics Engineers Inc. , 2019Conference paper, Published paper (Refereed)
Abstract [en]

Programming time-critical systems is notoriously difficult. In this paper we propose an actor-oriented programming model with a semantic notion of time and a deterministic coordination semantics based on discrete events to exercise precise control over both the computational and timing aspects of the system behavior.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers Inc., 2019
Keywords
Actors, Discrete events, Real-time systems, Aspect oriented programming, Computer aided design, Discrete time control systems, Interactive computer systems, Semantics, Precise control, Programming models, Programming time, System behaviors, Time-critical systems, Timing aspects, Real time systems
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-44871 (URN)10.1145/3316781.3323469 (DOI)2-s2.0-85067785090 (Scopus ID)9781450367257 (ISBN)
Conference
56th Annual Design Automation Conference, DAC 2019, 2 June 2019 through 6 June 2019
Available from: 2019-07-11 Created: 2019-07-11 Last updated: 2019-07-11Bibliographically approved
Causevic, A., Papadopoulos, A. & Sirjani, M. (2019). Towards a Framework for Safe and Secure Adaptive Collaborative Systems. In: The 9th IEEE International Workshop on Industrial Experience in Embedded Systems Design IEESD 2019: . Paper presented at The 9th IEEE International Workshop on Industrial Experience in Embedded Systems Design IEESD 2019, 15 Jul 2019, Milwaukee, Wisconsin, United States.
Open this publication in new window or tab >>Towards a Framework for Safe and Secure Adaptive Collaborative Systems
2019 (English)In: The 9th IEEE International Workshop on Industrial Experience in Embedded Systems Design IEESD 2019, 2019Conference paper, Published paper (Refereed)
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:mdh:diva-43936 (URN)
Conference
The 9th IEEE International Workshop on Industrial Experience in Embedded Systems Design IEESD 2019, 15 Jul 2019, Milwaukee, Wisconsin, United States
Projects
Future factories in the CloudSAFSEC-CPS -- Securing the safety of autonomous cyber-physical systemsSerendipity - Secure and dependable platforms for autonomy
Available from: 2019-06-20 Created: 2019-06-20 Last updated: 2019-06-20Bibliographically approved
de Berardinis, J., Forcina, G., Jafari, A. & Sirjani, M. (2018). Actor-based macroscopic modeling and simulation for smart urban planning. Science of Computer Programming, 168, 142-164
Open this publication in new window or tab >>Actor-based macroscopic modeling and simulation for smart urban planning
2018 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 168, p. 142-164Article in journal (Refereed) Published
Abstract [en]

Assessing the impacts of a mobility initiative prior to deployment is a complex task for both urban planners and transport companies. Computational models like Tangramob offer an agent-based framework for simulating the evolution of urban traffic after the introduction of new mobility services. However, simulations can be computationally expensive to perform due to their iterative nature and the microscopic representation of traffic. To address this issue, we designed a simplified model architecture of Tangramob in Timed Rebeca (TRebeca) and we developed a tool-chain for the generation runnable instances of this model starting from the same input files of Tangramob. Running TRebeca models allows users to get an idea of how the mobility initiatives under study affect the traveling experience of commuters, in a short time and without the need to use the simulator during this first experimental step. Then, once a subset of these initiatives is identified according to user's criteria, it is reasonable to simulate them with Tangramob in order to get more detailed results. To validate this approach, we compared the output of both the simulator and the TRebeca model on a collection of mobility initiatives. The correlation between the results demonstrates the usefulness of using TRebeca models for unconventional contexts of application.

Place, publisher, year, edition, pages
Elsevier B.V., 2018
Keywords
Actor-based modeling languages, Distributed computer systems, Modeling languages, Urban planning, Actor-based modeling, Agent-based framework, Computational model, Macroscopic model, Mobility service, Model architecture, Transport companies, Urban planners, Urban transportation
National Category
Computer Systems Embedded Systems
Identifiers
urn:nbn:se:mdh:diva-41015 (URN)10.1016/j.scico.2018.09.002 (DOI)000450385200007 ()2-s2.0-85053512327 (Scopus ID)
Available from: 2018-09-27 Created: 2018-09-27 Last updated: 2018-12-06Bibliographically approved
Khamespanah, E., Khosravi, R. & Sirjani, M. (2018). An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models. Science of Computer Programming, 153, 1-29
Open this publication in new window or tab >>An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models
2018 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 153, p. 1-29Article in journal (Refereed) Published
Abstract [en]

NP-hard time complexity of model checking algorithms for TCTL properties in dense time is one of the obstacles against using model checking for the analysis of real-time systems. Alternatively, a polynomial time algorithm is suggested for model checking of discrete time models against TCTL≤,≥ properties (i.e. TCTL properties without U=c modalities). The algorithm performs model checking against a given formula Φ for a state space with V states and E transitions in O(V(V+E)⋅|Φ|). In this work, we improve the model checking algorithm of TCTL≤,≥ properties, obtaining time complexity of O((Vlg⁡V+E)⋅|Φ|). We tackle the model checking of discrete timed actors as an application of the proposed algorithms. We show how the result of the fine-grained semantics of discrete timed actors can be model checked efficiently against TCTL≤,≥ properties using the proposed algorithm. This is illustrated using the timed actor modeling language Timed Rebeca. In addition to introducing a new efficient model checking algorithm, we propose a reduction technique which safely eliminates instantaneous transitions of transition systems (i.e. transition with zero time duration). We show that the reduction can be applied on-the-fly during the generation of the original timed transition system without a significant cost. We demonstrate the effectiveness of the reduction technique via a set of case studies selected from various application domains. Besides, while TCTL≤,≥ can be model checked in polynomial time, model checking of TCTL properties with U=c modalities is an NP-complete problem. Using the proposed reduction technique, we provide an efficient algorithm for model checking of complete TCTL properties over the reduced transition systems.

Place, publisher, year, edition, pages
Elsevier B.V., 2018
Keywords
Actor model, Durational transition graph, Model checking, TCTL, Timed Rebeca, Computational complexity, Interactive computer systems, Modeling languages, Polynomial approximation, Real time systems, Semantics, Actor models, Model checking algorithm, Polynomial-time algorithms, Reduction techniques, Timed transition systems, Transition graphs
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-38161 (URN)10.1016/j.scico.2017.11.004 (DOI)000424068300001 ()2-s2.0-85040332415 (Scopus ID)
Available from: 2018-01-22 Created: 2018-01-22 Last updated: 2018-02-15Bibliographically approved
Bagheri, M., Sirjani, M., Khamespanah, E., Khakpour, N., Akkaya, I., Movaghar, A. & Lee, E. A. (2018). Coordinated actor model of self-adaptive track-based traffic control systems. Journal of Systems and Software, 143, 116-139
Open this publication in new window or tab >>Coordinated actor model of self-adaptive track-based traffic control systems
Show others...
2018 (English)In: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 143, p. 116-139Article in journal (Refereed) Published
Abstract [en]

Self-adaptation is a well-known technique to handle growing complexities of software systems, where a system autonomously adapts itself in response to changes in a dynamic and unpredictable environment. With the increasing need for developing self-adaptive systems, providing a model and an implementation platform to facilitate integration of adaptation mechanisms into the systems and assuring their safety and quality is crucial. In this paper, we target Track-based Traffic Control Systems (TTCSs) in which the traffic flows through pre-specified sub-tracks and is coordinated by a traffic controller. We introduce a coordinated actor model to design self-adaptive TTCSs and provide a general mapping between various TTCSs and the coordinated actor model. The coordinated actor model is extended to build large-scale self-adaptive TTCSs in a decentralized setting. We also discuss the benefits of using Ptolemy II as a framework for model-based development of large-scale self-adaptive systems that supports designing multiple hierarchical MAPE-K feedback loops interacting with each other. We propose a template based on the coordinated actor model to design a self-adaptive TTCS in Ptolemy II that can be instantiated for various TTCSs. We enhance the proposed template with a predictive adaptation feature. We illustrate applicability of the coordinated actor model and consequently the proposed template by designing two real-life case studies in the domains of air traffic control systems and railway traffic control systems in Ptolemy II. 

Place, publisher, year, edition, pages
Elsevier Inc., 2018
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-40100 (URN)10.1016/j.jss.2018.05.034 (DOI)000438180000009 ()2-s2.0-85048497434 (Scopus ID)
Available from: 2018-06-28 Created: 2018-06-28 Last updated: 2018-08-17Bibliographically approved
Dastani, M., Hojjat, H. & Sirjani, M. (2018). Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2015) Preface. Science of Computer Programming, 160, 1-2
Open this publication in new window or tab >>Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2015) Preface
2018 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 160, p. 1-2Article in journal, Editorial material (Other academic) Published
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-39635 (URN)10.1016/j.scico.2017.11.006 (DOI)000432511400001 ()2-s2.0-85034864924 (Scopus ID)
Available from: 2018-06-07 Created: 2018-06-07 Last updated: 2018-07-25Bibliographically approved
Castagnari, C., de Berardinis, J., Forcina, G., Jafari, A. & Sirjani, M. (2018). Lightweight preprocessing for agent-based simulation of smart mobility initiatives. In: Lect. Notes Comput. Sci.: . Paper presented at 15th International Conference on Software Engineering and Formal Methods (SEFM),Fondazione Bruno Kessler, Trento, ITALY, EP 04-05, 2017 (pp. 541-557). Springer Verlag
Open this publication in new window or tab >>Lightweight preprocessing for agent-based simulation of smart mobility initiatives
Show others...
2018 (English)In: Lect. Notes Comput. Sci., Springer Verlag , 2018, p. 541-557Conference paper, Published paper (Refereed)
Abstract [en]

Understanding the impacts of a mobility initiative prior to deployment is a complex task for both urban planners and transport companies. To support this task, Tangramob offers an agent-based simulation framework for assessing the evolution of urban traffic after the introduction of new mobility services. However, Tangramob simulations are computationally expensive due to their iterative nature. Thus, we simplified the Tangramob model into a Timed Rebeca (TRebeca) model and we designed a tool-chain that generates instances of this model starting from the same Tangramob’s inputs. Running TRebeca models allows users to get an idea of how mobility initiatives affect the system performance, in a short time, without resorting to the simulator. To validate this approach, we compared the output of both the simulator and the TRebeca model on a collection of mobility initiatives. Results show a correlation between them, thus demonstrating the usefulness of using TRebeca models for unconventional contexts of application.

Place, publisher, year, edition, pages
Springer Verlag, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10729 LNCS
Keywords
Actor-based modeling languages, Agent-based simulations, Formal methods, Iterative methods, Modeling languages, Systems analysis, Urban transportation, Actor-based modeling, Agent based simulation, Complex task, Mobility service, Transport companies, Urban planners, Urban traffic, Software engineering
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-38795 (URN)10.1007/978-3-319-74781-1_36 (DOI)000432620300036 ()2-s2.0-85042067249 (Scopus ID)9783319747804 (ISBN)
Conference
15th International Conference on Software Engineering and Formal Methods (SEFM),Fondazione Bruno Kessler, Trento, ITALY, EP 04-05, 2017
Available from: 2018-03-01 Created: 2018-03-01 Last updated: 2018-06-07Bibliographically approved
Khamespanah, E., Sirjani, M., Mechitov, K. & Agha, G. (2018). Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking. Paper presented at 23rd International SPIN Symposium on Model Checking of Software (SPIN), APR 07-08, 2016, Eindhoven, NETHERLANDS. International Journal on Software Tools for Technology Transfer (STTT), 20(5), 547-561
Open this publication in new window or tab >>Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking
2018 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 20, no 5, p. 547-561Article in journal (Refereed) Published
Abstract [en]

Programmers often use informal worst-case analysis and debugging to ensure that schedulers satisfy real-time requirements. Not only can this process be tedious and error-prone, it is inherently conservative and thus likely to lead to an inefficient use of resources. We propose to use model checking to find a schedule which optimizes the use of resources while satisfying real-time requirements. Specifically, we represent a Wireless sensor and actuator network (WSAN) as a collection of actors whose behaviors are specified using a Java-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction mechanism and the compositionality of actors in the actor model may be used to incrementally build a model of a WSAN's behavior from node-level and network models. We demonstrate the approach with a case study of a distributed real-time data acquisition system for high-frequency sensing using Timed Rebeca modeling language and the Afra model checking tool.

Place, publisher, year, edition, pages
SPRINGER HEIDELBERG, 2018
Keywords
Sensor network, Schedulability analysis, Actor, Timed Rebeca, Model checking
National Category
Other Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-40736 (URN)10.1007/s10009-017-0480-3 (DOI)000441949300005 ()2-s2.0-85034566338 (Scopus ID)
Conference
23rd International SPIN Symposium on Model Checking of Software (SPIN), APR 07-08, 2016, Eindhoven, NETHERLANDS
Available from: 2018-09-06 Created: 2018-09-06 Last updated: 2018-11-28Bibliographically approved
Sirjani, M. (2018). Power is Overrated, Go for Friendliness! Expressiveness, Faithfulness, and Usability in Modeling: The Actor Experience. In: Lohstroh, Marten, Derler, Patricia, Sirjani, Marjan (Ed.), Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday. Paper presented at Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday (pp. 423-448). Paper presented at Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday. Springer Verlag
Open this publication in new window or tab >>Power is Overrated, Go for Friendliness! Expressiveness, Faithfulness, and Usability in Modeling: The Actor Experience
2018 (English)In: Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday / [ed] Lohstroh, Marten, Derler, Patricia, Sirjani, Marjan, Springer Verlag , 2018, p. 423-448Chapter in book (Refereed)
Abstract [en]

Expressive power of a language is generally defined as the breadth of ideas that can be represented and communicated in a language. For formal languages, the expressive power has been evaluated by checking its Turing completeness. In a modeling process, apart from the modeling language, we have two other counterparts: the system being modeled and the modeler. I argue that faithfulness to the system being modeled and usability for the modeler are at least as important as the expressive power of the modeling language, specially because most of the modeling languages used today are highly expressive. I call faithfulness and usability together “friendliness”. I show how we used the actor-based language Rebeca in modeling different applications, where it is friendly, and where it is not. I discuss how the friendliness of Rebeca may help in the analysis of models and allows for system synthesis on the basis of models. 

Place, publisher, year, edition, pages
Springer Verlag, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10760 LNCS
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-40922 (URN)10.1007/978-3-319-95246-8_25 (DOI)2-s2.0-85052704001 (Scopus ID)978-3-319-95246-8 (ISBN)
Conference
Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday
Available from: 2018-09-13 Created: 2018-09-13 Last updated: 2018-09-13Bibliographically approved
Organisations

Search in DiVA

Show all publications