SEADA - Self-Adaptive Actors
Status:
In SEADA, we propose a framework for self-adaptive systems with a component-based architecture built in Ptolemy II that forms the feedback loop. Our models@runtime are coded in Timed Rebeca. Supporting tools for customized runtime formal verification of these models are developed. Our focus is on safety assurance while addressing uncertainty and responsiveness of the applications. SEADA benefits from using Ptolemy in various ways. Ptolemy gives us the support for modeling cyber-physical systems; hence interaction with the physical world can be done smoothly. Furthermore, connecting Ptolemy actors and Rebeca actors can be done in a natural way, so, keeping the model@runtime up-to-date using Ptolemy event queues takes the least effort. The distinctive feature of SEADA is its actor-based flavor which will reflect in the design of the components of the architecture, the models in the knowledge-base, and in the V&V and formal verification techniques. In developing SEADA models we focus on the air traffic control and flight network applications. These applications are safety critical, and highly sensitive to changes that can occur in the system and the environment.
| First Name | Last Name | Title |
|---|---|---|
| Marjan | Sirjani | Professor |
| Narges | Khakpour | Associate Professor |
| Edward | Lee | Visiting Professor |
| Maryam | Bagheri | Doctoral student |
| Ali | Jafari | Researcher |
| Carolyn | Talcott | Research project manager |
| Ehsan | Khamespanah | Assistant Professor |
Safe Design of Flow Management Systems Using Rebeca (Sep 2020) Giorgio Forcina, Ali Sedaghatbaf, Stephan Baumgart, Ali Jafari , Ehsan Khamespanah , Pavle Mrvaljevic , Marjan Sirjani Journal of Information Processing (IPSJ)
VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance (Jun 2020) Farnaz Yousefi , Ehsan Khamespanah , Mohammed Gharib , Marjan Sirjani, Ali Movaghar International Journal on Software Tools for Technology Transfer (STTT)
