| 1. |
- Lohstroh, M., et al.
(author)
-
Invited : Actors revisited for time-critical systems
- 2019
-
In: Proceedings - Design Automation Conference. - New York, NY, USA : Institute of Electrical and Electronics Engineers Inc.. - 9781450367257
-
Conference paper (peer-reviewed)abstract
- Programming time-critical systems is notoriously difficult. In this paper we propose an actor-oriented programming model with a semantic notion of time and a deterministic coordination semantics based on discrete events to exercise precise control over both the computational and timing aspects of the system behavior.
|
|
| 2. |
- Bagheri, M., et al.
(author)
-
Partial Order Reduction for Timed Actors
- 2022
-
In: Lect. Notes Comput. Sci.. - Cham : Springer Science and Business Media Deutschland GmbH. - 9783030955601 ; , s. 43-60
-
Conference paper (peer-reviewed)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.
|
|
| 3. |
- Bagheri, M., et al.
(author)
-
Runtime compositional analysis of track-based traffic control systems
- 2017
-
In: ACM SIGBED Review. - : Association for Computing Machinery (ACM). - 1551-3688. ; 14:3, s. 38-39
-
Journal article (peer-reviewed)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.
|
|
| 4. |
- Dastani, M., et al.
(author)
-
Preface
- 2017
-
In: Lect. Notes Comput. Sci.. - : Springer Verlag. - 9783319689715
-
Conference paper (other academic/artistic)
|
|
| 5. |
- Dehnavi, S., et al.
(author)
-
Towards an actor-based approach to design verified ROS-based robotic programs using rebeca
- 2019
-
In: Procedia Computer Science. - : Elsevier B.V.. - 1877-0509. ; , s. 59-68
-
Conference paper (peer-reviewed)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. |
- Ghassemi, F., et al.
(author)
-
Transparent Actor Model
- 2023
-
In: 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
-
Conference paper (peer-reviewed)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.
|
|
| 7. |
- Hojjat, H., et al.
(author)
-
Process algebraic verification of SystemC codes
- 2008
-
In: Application of Concurrency to System Design, 2008. ACSD 2008. 8th International Conference on. - New York : IEEE Press. - 9781424418381 - 9781424418398 ; , s. 62-67
-
Conference paper (peer-reviewed)abstract
- SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC codes by providing a mapping to the process algebra mCRL2. The outstanding advantages of mCRL2 are the support for different data types and a powerful tool-set for model reduction and analysis. A tool is implemented to automatically perform the proposed mapping. This translation enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.
|
|
| 8. |
- Hojjat, H., et al.
(author)
-
Sarir : a Rebeca to mCRL2 translator
- 2007
-
In: Application of Concurrency to System Design, 2007. ACSD 2007. Seventh International Conference on. - Los Alamitos, Calif. : IEEE Computer Society. - 076952902X - 9780769529028 ; , s. 216-220
-
Conference paper (peer-reviewed)abstract
- We describe a translation from Rebeca, an actor-based language, to mCRL2, a process algebra enhanced with data types. The main motivation is to exploit the verification tools and theories developed for mCRL2 in Rebeca. The mapping is applied to several case-studies including the tree identify phase of the IEEE 1394 standard. The results of the experiment show that the minimization tools of mCRL2 can be very effective and the outcome of the present translation outperforms that of the translation to the input language of the Spin model-checker.
|
|
| 9. |
- Khakpour, Narges, et al.
(author)
-
PobSAM : policy-based managing of actors in self-adaptive systems
- 2010
-
In: Proceedings of the 6th International Workshop on Formal Aspects of Component Software (FACS’09, Eindhoven, The Netherlands, November 2-3, 2009). - Amsterdam : Elsevier. ; 263, s. 129-143
-
Conference paper (peer-reviewed)
|
|
| 10. |
- Lohstroh, M., et al.
(author)
-
Preface
- 2018
-
In: Principles of Modeling. - : Springer Verlag. - 9783319952468 ; , s. VII-X
-
Book chapter (other academic/artistic)
|
|
