| 1. |
- Bagheri, Maryam, et al.
(författare)
-
Coordinated actor model of self-adaptive track-based traffic control systems
- 2018
-
Ingår i: Journal of Systems and Software. - : Elsevier. - 0164-1212 .- 1873-1228. ; 143, s. 116-139
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 2. |
- Bagheri, Maryam, et al.
(författare)
-
Coordinated actors for reliable self-adaptive systems
- 2017
-
Ingår i: FACS 2016. - Cham : Springer. - 9783319576657 - 9783319576664 ; , s. 241-259
-
Konferensbidrag (refereegranskat)abstract
- Self-adaptive systems are systems that automatically adapt in response to environmental and internal changes, such as possible failures and variations in resource availability. Such systems are often realized by a MAPE-K feedback loop, where Monitor, Analyze, Plan and Execute components have access to a runtime model of the system and environment which is kept in the Knowledge component. In order to provide guarantees on the correctness of a self-adaptive system at runtime, the MAPE-K feedback loop needs to be extended with assurance techniques. To address this issue, we propose a coordinated actor-based approach to build a reusable and scalable model@runtime for self-adaptive systems in the domain of track-based traffic control systems. We demonstrate the approach by implementing an automated Air Traffic Control system (ATC) using Ptolemy tool.We compare different adaptation policies on the ATC model based on performance metrics and analyze combination of policies in different configurations of the model. We enriched our framework with runtime performance analysis such that for any unexpected change, subsequent behavior of the model is predicted and results are used for adaptation at the change-point. Moreover, the developed framework enables checking safety properties at runtime. © Springer International Publishing AG 2017.
|
|
| 3. |
- Bagheri, Maryam, et al.
(författare)
-
Lightweight Formal Method for Robust Routing in Track-based Traffic Control Systems
- 2020
-
Ingår i: 2020 18TH ACM-IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN (MEMOCODE). - : IEEE. ; , s. 115-124
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we propose a robust solution for the path planning and scheduling of the moving objects in a Track-based Traffic Control System (TTCS). The moving objects in a TTCS pass over pre-specified sub-tracks. Each sub-track accommodates at most one moving object in-transit. Due to the uncertainties in the context of a TTCS, we assign an arrival time window to each moving object for each sub-track in its route, instead of an exact value. The moving object can safely enter into the sub-track in the mentioned time window. To develop a safe plan, we adapt the tagged-signal model and provide a rigorous mathematical formalism for the actor model of a TTCS. To illustrate the applicability of the provided semantics, we provide a formal model of TTCSs in the Alloy language and use its analyzer to verify the developed model against system safety properties.
|
|
| 4. |
- Bagheri, Maryam, et al.
(författare)
-
Magnifier : A Compositional Analysis Approach for Autonomous Traffic Control
- 2022
-
Ingår i: IEEE Transactions on Software Engineering. - 0098-5589 .- 1939-3520. ; 48:8, s. 2732-2747
-
Tidskriftsartikel (refereegranskat)abstract
- Autonomous traffic control systems are large-scale systems with critical goals. To satisfy expected properties, these systems adapt themselves to possible changes in their environment and in the system itself. The adaptation may result in further changes propagated throughout the system. For each change and its consequent adaptation, assuring the satisfaction of properties of the system at runtime is important. A prominent approach to assure the correct behavior of these systems is verification at runtime, which has strict time and memory limitations. To tackle these limitations, we propose Magnifier, an iterative, incremental, and compositional verification approach that operates on an actor-based model where actors are grouped in components, and components are augmented with a coordinator. The Magnifier idea is zooming on the area (component) affected by a change and verifying the correctness of properties of interest of the system after adapting the component to the change. Magnifier checks if the change is propagating, and if that is the case, then it zooms out to perform adaptation on a larger area to contain the change. The process is iterative and incremental, and considers areas affected by the change one by one. In Magnifier, we use the Coordinated Adaptive Actor model (CoodAA) for traffic control systems. We present a formal semantics for CoodAA as a network of Timed Input-Output Automata (TIOAs), and prove the correctness of our compositional reasoning. We implement our approach in Ptolemy II. The results of our experiments indicate that the proposed approach improves the verification time and the memory consumption compared to the non-compositional approach.
|
|
| 5. |
- De Boer, Frank, et al.
(författare)
-
A Survey of Active Object Languages
- 2017
-
Ingår i: ACM Computing Surveys. - : ASSOC COMPUTING MACHINERY. - 0360-0300 .- 1557-7341. ; 50:5
-
Tidskriftsartikel (refereegranskat)abstract
- To program parallel systems efficiently and easily, a wide range of programming models have been proposed, eachwith different choices concerning synchronization and communication between parallel entities. Among them, the actor model is based on loosely coupled parallel entities that communicate by means of asynchronous messages and mailboxes. Some actor languages provide a strong integration with object-oriented concepts; these are often called active object languages. This article reviews four major actor and active object languages and compares them according to carefully chosen dimensions that cover central aspects of the programming paradigms and their implementation.
|
|
| 6. |
- Jafari, Ali, et al.
(författare)
-
PTRebeca : Modeling and analysis of distributed and asynchronous systems
- 2016
-
Ingår i: Science of Computer Programming. - : Elsevier BV. - 0167-6423 .- 1872-7964. ; 128, s. 22-50
-
Tidskriftsartikel (refereegranskat)abstract
- Distributed systems exhibit probabilistic and non-deterministic behaviors and may have time constraints. Probabilistic Timed Rebeca (PTRebeca) is introduced as a timed and probabilistic actor-based language for modeling distributed real-time systems with asynchronous message passing. The semantics of PTRebeca is a Timed Markov Decision Process. In this paper, we provide SOS rules for PTRebeca, introduce a new tool-set and describe the corresponding mappings. The tool-set automatically generates a Markov Automaton from a PTRebeca model in the form of the input language of the Interactive Markov Chain Analyzer (IMCA). The IMCA can be used as a back-end model checker for performance analysis of PTRebeca models against expected reachability and probabilistic reachability properties. Comparing to the existing tool-set, proposed in the conference paper, we now have the ability of analyzing significantly larger models, and we also can add different rewards to the model. We show the applicability of our approach and efficiency of our tool by analyzing a Network on Chip architecture as a real-world case study. (C) 2016 Elsevier B.V. All rights reserved.
|
|
| 7. |
- Jafari, Ali, et al.
(författare)
-
Statistical model checking of Timed Rebeca models
- 2016
-
Ingår i: Computer languages, systems & structures. - : Elsevier BV. - 1477-8424 .- 1873-6866. ; 45, s. 53-79
-
Tidskriftsartikel (refereegranskat)abstract
- The actor-based language, Timed Rebeca, was introduced to model distributed and asynchronous systems with timing constraints and message passing communication. A toolset was developed for automated translation of Timed Rebeca models to Erlang. The translated code can be executed using a timed extension of McErlang for model checking and simulation. In this work, we added a new toolset that provides statisticalmodel checking of Timed Rebeca models. Using statistical model checking, we are now able to verify larger models against safety properties compared to McErlang model checking. We examine the typical case studies of elevators and ticket service to show the efficiency of statisticalmodel checking and applicability of our toolset.
|
|
| 8. |
- Jaghoori, Mohammad Mahdi, et al.
(författare)
-
Symmetry and partial order reduction techniques in model checking Rebeca
- 2010
-
Ingår i: Acta Informatica. - New York : Springer. - 0001-5903 .- 1432-0525. ; 47:1, s. 33-66
-
Tidskriftsartikel (refereegranskat)abstract
- Rebeca is an actor-based language with formal semantics which is suitable for modeling concurrent and distributed systems and protocols. Due to its object model, partial order and symmetry detection and reduction techniques can be efficiently applied to dynamic Rebecamodels. We present two approaches for detecting symmetry in Rebeca models: One that detects symmetry in the topology of inter-connections among objects and another one which exploits specific data structures to reflect internal symmetry in the internal structure of an object. The former approach is novel in that it does not require any input from the modeler and can deal with the dynamic changes of topology. This approach is potentially applicable to a wide range of modeling languages for distributed and reactive systems. We have also developed a model checking tool that implements all of the above-mentioned techniques. The evaluation results show significant improvements in model size and model-checkingtime.
|
|
| 9. |
- Khamespanah, Ehsan, et al.
(författare)
-
Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking
- 2018
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 20:5, s. 547-561
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 10. |
- Khamespanah, Ehsan, et al.
(författare)
-
Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking
- 2016
-
Ingår i: Model Checking Software - 23rd International Symposium SPIN 2016. - Cham : Springer International Publishing. - 9783319325811 ; , s. 165-181
-
Konferensbidrag (refereegranskat)abstract
- Programmers often use informal worst-case analysis and debugging to ensure schedules that 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 behavior is specified using a C-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction and compositionality properties of 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.
|
|
