| 1. |
- 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.
|
|
| 2. |
- 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.
|
|
| 3. |
- 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.
|
|
| 4. |
- 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)
|
|
| 5. |
- Ebrahimi, E., et al.
(författare)
-
Model Checking of Hyperledger Fabric Smart Contracts
- 2023
-
Ingår i: IEEE Int. Conf. Emerging Technol. Factory Autom., ETFA. - : Institute of Electrical and Electronics Engineers Inc.. - 9798350339918
-
Konferensbidrag (refereegranskat)abstract
- Conducting interactions between shared-purpose organizations that are not entirely trustworthy of each other without centralized oversight is an idea that emerged with the advent of private blockchains such as Hyperledger Fabric and its smart contracts. It is critical to check contracts to ensure their proper functionality, as organizations may collaborate with competitors. Due to the new architecture of Hyperledger Fabric, tools in this area are limited. To formally verify the source code of contracts, we mapped Fabric contract concepts into the Rebeca modeling language. Rebeca is an actor-based language that enables the modeling of concurrent and distributed systems and is supported by a model checking tool, Afra. We have identified vulnerabilities such as deadlock and starvation by examining the desired properties. Using the model checking approach, we could debug the code and hence benefit from speeding up the transactions, creating fewer extra blocks, requiring less storage space to store the ledger, and avoiding wasting computing resources.
|
|
| 6. |
- Forcina, Giorgio, et al.
(författare)
-
Safe design of flow management systems using rebeca
- 2020
-
Ingår i: Journal of Information Processing. - : Information Processing Society of Japan. - 0387-5806 .- 1882-6652. ; 28, s. 588-598
-
Tidskriftsartikel (refereegranskat)abstract
- Track-based flow management systems like transportation systems and traffic control systems play a crucial role in our daily life. Safety and performance are among the most important quality requirements for these systems. This paper presents AdaptiveFlow as a framework for modeling, safety checking and performance analysis of track-based flow management systems. AdaptiveFlow is based on the Hewitt actors computation model. In particular, tracks are modeled as actors and moving objects as messages. Timed Rebeca is used for modeling, and the model checking tool Afra is used for safety verification and performance evaluation in AdaptiveFlow. To react to dynamic changes in the environment, AdaptiveFlow provides support for three adaptive policies, which can be examined and compared in different scenarios. To demonstrate the applicability of AdaptiveFlow, we consider the Electric Site Research Project of Volvo Construction Equipment as a case study. In this project, a fleet of autonomous haulers is utilized to transport materials in a quarry site. Furthermore, to show the reusability of the framework for other flow management scenarios, an experiment on an urban garbage collection system is presented. © 2020 Information Processing Society of Japan.
|
|
| 7. |
- Ghassemi, F., et al.
(författare)
-
Transparent Actor Model
- 2023
-
Ingår i: Proceedings - 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering, FormaliSE 2023. - : Institute of Electrical and Electronics Engineers Inc.. - 9798350312638 ; , s. 97-107
-
Konferensbidrag (refereegranskat)abstract
- Several programming and formal modeling languages are designed based on actors. Each language has certain policies for message delivery between actors and for handling the messages in the buffers. These policies are implicit in the semantics of each language. One can infer interesting properties of actor languages related to communication and coordination based on different policies and their interactions. We define the 'Transparent Actor' model where we make policies explicit as points of possible variations. We identify an abstract network entity and define the semantics of Transparent Actors in three parts: actors, network, and composition. We define a core actor language named BABEL as a basis to describe the semantics of Transparent Actors using structural operational semantics (SOS) rules with variation points. These parametric rules make the implicit policies clear and can be used as a template to define the semantics of different actor-based languages. We evaluate the applicability of the template by examining the semantics for actor-based languages Rebeca, Lingua Franca, ABS, AKKA, and Erlang. We implement BABEL in Maude as a proof of concept, then concretize the parametric rules to implement some of the above languages. We consider a few properties, check them via a set of designated litmus test cases using our Maude implementations, and discuss the policy interactions.
|
|
| 8. |
- Jahandideh, Iman, et al.
(författare)
-
An actor-based framework for asynchronous event-based cyber-physical systems
- 2021
-
Ingår i: Software and Systems Modeling. - : SPRINGER HEIDELBERG. - 1619-1366 .- 1619-1374. ; 20:3, s. 641-665
-
Tidskriftsartikel (refereegranskat)abstract
- 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 actors supports modeling distributed asynchronously communicating systems. We propose the Hybrid Rebeca language to support the modeling of cyber-physical systems. Hybrid Rebeca is an extension of the 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 develop a tool to derive hybrid automata as the basis for the analysis of Hybrid Rebeca models. We demonstrate the applicability of our approach through a case study in the domain of automotive systems. We use the SpaceEx framework for reachability analysis of the case study. Compared to hybrid automata, our results show that for event-based asynchronous models hybrid Rebeca improves analyzability by reducing the number of real variables, and increases modularity and hence, minimizes the number of changes caused by a modification in the model.
|
|
| 9. |
- Johansson, Bjarne, et al.
(författare)
-
Formal Verification of Consistency for Systems with Redundant Controllers
- 2024
-
Ingår i: Electronic Proceedings in Theoretical Computer Science, EPTCS. - : Open Publishing Association. ; , s. 169-191
-
Konferensbidrag (refereegranskat)abstract
- A potential problem that may arise in the domain of distributed control systems is the existence of more than one primary controller in redundancy plans that may lead to inconsistency. An algorithm called NRP FD is proposed to solve this issue by prioritizing consistency over availability. In this paper, we demonstrate how by using modeling and formal verification, we discovered an issue in NRP FD where we may have two primary controllers at the same time. We then provide a solution to mitigate the identified issue, thereby enhancing the robustness and reliability of such systems.
|
|
| 10. |
- Khamespanah, E., et al.
(författare)
-
Afra : An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family Models
- 2023
-
Ingår i: Lect. Notes Comput. Sci.. - : Springer Science and Business Media Deutschland GmbH. - 9783031424403 ; , s. 72-87
-
Konferensbidrag (refereegranskat)abstract
- Afra is an Eclipse-based tool for the modeling and model checking of Rebeca family models. Together with the standard enriched editor, easy to trace counter-example viewer, modular temporal property definition, exporting a model and its transition system to some other formats facilities are features of Afra. Rebeca family provides actor-based modeling languages which are designed to bridge the gap between formal methods and software engineering. Faithfulness to the system being modeled, and the usability of Rebeca family languages help in ease of modeling and analysis of the model, together with the synthesis of the system based on the model. In this paper, architectural decisions and design strategies we made in the development of Afra are presented. This makes Afra an extensible and reusable application for the modeling and analysis of Rebeca family models. Here, we show how different compilers can be developed for the family of languages which are the same in general language constructs but have some minor differences. Then we show how the model checking engine for these different languages is designed. Despite the fact that Afra has a layered object-oriented design and is developed in Java technology, we use C++ codes for developing its model checking for the performance purposes. This decision made the design of the application even harder.
|
|
