| 1. |
- 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.
|
|
| 2. |
- 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.
|
|
| 3. |
- Sirjani, Marjan, et al.
(författare)
-
Model Checking Software in Cyberphysical Systems
- 2020
-
Ingår i: Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020. - : Institute of Electrical and Electronics Engineers Inc.. - 9781728173030 ; , s. 1017-1026
-
Konferensbidrag (refereegranskat)abstract
- Model checking a software system is about verifying that the state trajectory of every execution of the software satisfies formally specified properties. The set of possible executions is modeled as a transition system. Each 'state' in the transition system represents an assignment of values to variables, and a state trajectory (a path through the transition system) is a sequence of such assignments. For cyberphysical systems (CPSs), however, we are more interested in the state of the physical system than the values of the software variables. The value of model checking the software therefore depends on the relationship between the state of the software and the state of the physical system. This relationship can be complex because of the real-time nature of the physical plant, the sensors and actuators, and the software that is almost always concurrent and distributed. In this paper, we study different ways to construct a transition system model for the distributed and concurrent software components of a CPS. We describe a logical-time based transition system model, which is commonly used for verifying programs written in synchronous languages, and derive the conditions under which such a model faithfully reflects physical states. When these conditions are not met (a common situation), a finer-grained event-based transition system model may be required. Even this finer-grained model, however, may not be sufficiently faithful, and the transition system model needs to be refined further to express not only the properties of the software, but also the properties of the hardware on which it runs. We illustrate these tradeoffs using a coordination language called Lingua Franca that is well-suited to extracting transition system models at these various levels of granularity, and we extend the Timed Rebeca language and its tool Afra to perform this extraction and then to perform model checking.
|
|
| 4. |
- 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.
|
|
| 5. |
- Dehnavi, S., et al.
(författare)
-
Towards an actor-based approach to design verified ROS-based robotic programs using rebeca
- 2019
-
Ingår i: Procedia Computer Science. - : Elsevier B.V.. - 1877-0509. ; , s. 59-68
-
Konferensbidrag (refereegranskat)abstract
- Robotic technology helps humans in different areas such as manufacturing, health care and education. Due to the ubiquitous revolution, today's focus is on mobile robots and their applications in a variety of cyber-physical systems. ROS is a wll-known and powerful middleware that facilitates software development for mobile robots. However, this middleware does not support assuring properties such as timeliness and safety of ROS-based software. In this paper we present an integration of Timed Rebeca modeling language with ROS to synthesize verified robotic software. First, a conceptual model of robotic programs is developed using Timed Rebeca. After verifying a set of user-defined correctness properties on this model, it is translated to a ROS program automatically. Experiments on some small-scale case studies illustrates the applicability of the proposed integration method.
|
|
| 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. |
- 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.
|
|
| 9. |
- Khamespanah, E., et al.
(författare)
-
An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models
- 2018
-
Ingår i: Science of Computer Programming. - : Elsevier B.V.. - 0167-6423 .- 1872-7964. ; 153, s. 1-29
-
Tidskriftsartikel (refereegranskat)abstract
- 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((VlgV+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.
|
|
| 10. |
- Khosravi, R., et al.
(författare)
-
Actors Upgraded for Variability, Adaptability, and Determinism
- 2024
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - : Springer Science and Business Media Deutschland GmbH. ; , s. 226-260
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- The Rebeca modeling language is designed as an imperative actor-based language with the goal of providing an easy-to-use language for modeling concurrent and distributed systems, with formal verification support. Rebeca has been extended to support time and probability. We extend Rebeca further with inheritance, polymorphism, interface declaration, and annotation mechanisms. These features allow us to handle variability within the model, support non-disruptive model evolution, and define method priorities. This enables Rebeca to be used more effectively in different domains, like in Software Product Lines, and holistic analysis of Cyber-Physical Systems. We develop specialized analysis techniques to support these extensions, partly integrated into Afra, the model checking tool of Rebeca.
|
|
| 11. |
- Rezaei, S., et al.
(författare)
-
Developing Safe Smart Contracts
- 2020
-
Ingår i: Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020. - : Institute of Electrical and Electronics Engineers Inc.. - 9781728173030 ; , s. 1027-1035
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- Blockchain is a shared, distributed ledger on which transactions are digitally recorded and linked together. Smart Contracts are programs running on Blockchain and are used to perform transactions in a distributed environment without need for any trusted third party. Since smart contracts are used to transfer assets between contractual parties, their safety and security are crucial and badly written and insecure contracts may result in catastrophe. Actor-based programming is known to solve several problems in building distributed software systems. Moreover, formal verification is a solid technique for developing dependable systems. In this paper, we show how the actor model can be used for modeling, analysis and synthesis of smart contracts. We propose Smart Rebeca as an extension of the actor-based language Rebeca, and use the model checking toolset Afra for verification of smart contracts. We implement a synthesizer to synthesize Solidity programs that run on the Ethereum platform from Smart Rebeca models. We examine the challenges and opportunities of our approach in modeling, formal verification, and synthesis of smart contracts using actors.
|
|
| 12. |
- Sharifi, Z., et al.
(författare)
-
Towards Formal Analysis of Vehicle Platoons Using Actor Model
- 2020
-
Ingår i: IEEE International Conference on Emerging Technologies and Factory Automation, ETFA. - : Institute of Electrical and Electronics Engineers Inc.. - 9781728189567 ; , s. 1820-1827
-
Konferensbidrag (refereegranskat)abstract
- Vehicle platooning is a promising technology to save the road capacity and also fuel consumption by reducing the distance between the vehicles in the platoon. The closer the cars are to each other, the closer we are to the goals. But, this will increase the need for safety verification. In this paper we use formal methods to verify safety distance in a platoon. To do so, we present a formal actor-based model for a vehicle platoon which incorporates vehicle dynamics and communication protocol. Also, we present a method to do the analysis based on model checking that applies mathematical analysis to reduce the state space. The method uses an upper bound and a lower bound value as network delay, and verifies if a specified vehicle in a platoon has enough distance to the leader during its traveling. © 2020 IEEE.
|
|
| 13. |
- Sirjani, Marjan, et al.
(författare)
-
Reactive Actors : Isolation for Efficient Analysis of Distributed Systems
- 2019
-
Ingår i: Proceedings - 2019 IEEE/ACM 23rd International Symposium on Distributed Simulation and Real Time Applications, DS-RT 2019. - : Institute of Electrical and Electronics Engineers Inc.. - 9781728129235
-
Konferensbidrag (refereegranskat)abstract
- In this paper we explain how the isolation or decoupling of actors can help in developing efficient analysis techniques. The Reactive Object Language, Rebeca, and its timed extension are introduced as actor-based languages for modeling and analyzing distributed systems. We show how floating-time transition system can be used for model checking of timed actor models when we are interested in event-based properties, and how it helps in state space reduction. We explain how the model of computation of actors helps in devising an efficient state distribution policy in distributed model checking. We show how we use Rebeca to verify the routing algorithms of mobile adhoc networks. The paper is written in a way to make the ideas behind each technique clear such that it can be reused in similar domains.
|
|
| 14. |
- Sirjani, Marjan, et al.
(författare)
-
Timed Actors and Their Formal Verification
- 2023
-
Ingår i: Electronic Proceedings in Theoretical Computer Science, EPTCS. - : Open Publishing Association. ; , s. 1-7
-
Konferensbidrag (refereegranskat)abstract
- In this paper we review the actor-based language, Timed Rebeca, with a focus on its formal semantics and formal verification techniques. Timed Rebeca can be used to model systems consisting of encapsulated components which communicate by asynchronous message passing. Messages are put in the message buffer of the receiver actor and can be seen as events. Components react to these messages/events and execute the corresponding message/event handler. Real-time features, like computation delay, network delay and periodic behavior, can be modeled in the language. We explain how both Floating-Time Transition System (FTTS) and common Timed Transition System (TTS) can be used as the semantics of such models and the basis for model checking. We use FTTS when we are interested in event-based properties, and it helps in state space reduction. For checking the properties based on the value of variables at certain point in time, we use the TTS semantics. The model checking toolset supports schedulability analysis, deadlock and queue-overflow check, and assertion based verification of Timed Rebeca models. TCTL model checking based on TTS is also possible but is not integrated in the tool.
|
|
