mdh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Sirjani, Marjan
Publications (10 of 13) Show all publications
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
Lohstroh, M., Derler, P. & Sirjani, M. (2018). Preface. In: Lohstroh, Marten, Derler, Patricia, Sirjani, Marjan (Ed.), Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday (pp. VII-X). Springer Verlag
Open this publication in new window or tab >>Preface
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. VII-XChapter in book (Other academic)
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-40924 (URN)2-s2.0-85052701732 (Scopus ID)978-3-319-95246-8 (ISBN)
Available from: 2018-09-13 Created: 2018-09-13 Last updated: 2018-09-13Bibliographically approved
Sirjani, M., Ghassemi, F. & Pourvatan, B. (2018). Reo connectors and components as tagged signal models. In: It's All About Coordination: Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab (pp. 160-173). Springer
Open this publication in new window or tab >>Reo connectors and components as tagged signal models
2018 (English)In: It's All About Coordination: Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab, Springer, 2018, p. 160-173Chapter in book (Refereed)
Abstract [en]

Tagged Signal Model (TSM) is a denotational framework and a meta-model to study certain properties of models of computation. To study the behavior of Reo connectors in a closed system, we propose two denotational semantics for Reo using TSM. TSM is very similar to the coalgebraic model of Timed Data Streams (TDS), the first formal semantics and the basis for most of the other formal semantics of Reo. There is a direct mapping between the time – data pairs of TDS, and tag – value of TSM. This work shows how treating tags to be either totally or partially ordered has a direct consequence on the results. We looked into five primitive connectors of Reo in both these settings and discuss the determinacy of systems. 

Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10865 LNCS
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-39821 (URN)10.1007/978-3-319-90089-6_11 (DOI)2-s2.0-85047799414 (Scopus ID)9783540223818 (ISBN)
Available from: 2018-06-14 Created: 2018-06-14 Last updated: 2018-06-14Bibliographically approved
Jafari, A., Nair, J. J., Baumgart, S. & Sirjani, M. (2018). Safe and efficient fleet operation for autonomous machines: An actor-based approach. In: Proceedings of the ACM Symposium on Applied Computing: . Paper presented at 33rd Annual ACM Symposium on Applied Computing, SAC 2018, 9 April 2018 through 13 April 2018 (pp. 423-426).
Open this publication in new window or tab >>Safe and efficient fleet operation for autonomous machines: An actor-based approach
2018 (English)In: Proceedings of the ACM Symposium on Applied Computing, 2018, p. 423-426Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we formally model and verify run-time requirements of an application consisting of complex electrified machines called HX autonomous haulers, developed by Volvo Construction Equipment. To model the fleet control, we use Timed Rebeca, an actor-based modeling language, and to analyze the system performance, we use Afra, an integrated environment for modeling and verifying distributed systems modeled by Rebeca or Timed Rebeca language. We run a set of experiments to find the improved configuration in which the total time for machines to complete one operating cycle is minimized. 

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-40371 (URN)10.1145/3167132.3167382 (DOI)2-s2.0-85050546231 (Scopus ID)9781450351911 (ISBN)
Conference
33rd Annual ACM Symposium on Applied Computing, SAC 2018, 9 April 2018 through 13 April 2018
Available from: 2018-08-16 Created: 2018-08-16 Last updated: 2018-08-16Bibliographically approved
Organisations

Search in DiVA

Show all publications