In SEADA, we will propose a framework for self-adaptive systems with a component-based architecture built in Ptolemy II that forms the feedback loop. Our models@runtime will be coded in an extension of Probabilistic Timed Rebeca (with dynamic features). Supporting tools for customized run- time formal verification of these models will be developed. Our focus will be on safety assurance while addressing uncertainty and responsiveness of the applications. SEADA will benefit 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.
Maryam Bagheri, Marjan Sirjani, Ehsan Khamespanah, Narges Khakpour, Ilge Akkaya, Ali Movaghar and Edward A. Lee: Coordinated Actor Model of Self-adaptive Track-based Traffic Control Systems, Journal of Systems and Software, 2018 [pdf]
Maryam Bagheri, Ehsan Khamespanah, Marjan Sirjani, Ali Movaghar, Edward A. Lee: Runtime Compositional Analysis of Track-based Traffic Control Systems, CRTS, 2016 [pdf]
Maryam Bagheri, Ilge Akkaya, Ehsan Khamespanah, Narges Khakpour, Marjan Sirjani, Ali Movaghar, Edward A. Lee: Modeling and Analyzing Air Traffic Control Systems using Ptolemy, Ptolemy Mini-Conference, 2015 [pdf]