| 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. |
- Bagheri, M., et al.
(författare)
-
Partial Order Reduction for Timed Actors
- 2022
-
Ingår i: Lect. Notes Comput. Sci.. - Cham : Springer Science and Business Media Deutschland GmbH. - 9783030955601 ; , s. 43-60
-
Konferensbidrag (refereegranskat)abstract
- We propose a compositional approach for the Partial Order Reduction (POR) in the state space generation of asynchronous timed actors. We define the concept of independent actors as the actors that do not send messages to a common actor. The approach avoids exploring unnecessary interleaving of executions of independent actors. It performs on a component-based model where actors from different components, except for the actors on borders, are independent. To alleviate the effect of the cross-border messages, we enforce a delay condition, ensuring that an actor introduces a delay in its execution before sending a message across the border of its component. Within each time unit, our technique generates the state space of each individual component by taking its received messages into account. It then composes the state spaces of all components. We prove that our POR approach preserves the properties defined on timed states (states where the only outgoing transition shows the progress of time). We generate the state space of a case study in the domain of air traffic control systems based on the proposed POR. The results on our benchmarks illustrate that our POR method, on average, reduces the time and memory consumption by 76 and 34%, respectively.
|
|
| 6. |
- Bagheri, M., et al.
(författare)
-
Runtime compositional analysis of track-based traffic control systems
- 2017
-
Ingår i: ACM SIGBED Review. - : Association for Computing Machinery (ACM). - 1551-3688. ; 14:3, s. 38-39
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper we address the development of dependable self-adaptive systems focusing on the specific domain of track-based traffic control systems where timing issues are critical.
|
|
| 7. |
- Biffl, S., et al.
(författare)
-
Preface
- 2021
-
Ingår i: Lect. Notes Comput. Sci.. - : Springer Science and Business Media Deutschland GmbH. - 9783030860431 ; , s. v-vi
-
Konferensbidrag (refereegranskat)
|
|
| 8. |
- Castagnari, C., et al.
(författare)
-
Lightweight preprocessing for agent-based simulation of smart mobility initiatives
- 2018
-
Ingår i: Lect. Notes Comput. Sci.. - Cham : Springer Verlag. - 9783319747804 ; , s. 541-557
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 9. |
|
|
| 10. |
- Cimatti, A., et al.
(författare)
-
Preface
- 2017
-
Ingår i: Lect. Notes Comput. Sci.. - : Springer Verlag. - 9783319661964 ; , s. V-VI
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)
|
|
