SEADA: Self-Adaptive Actors

Description

We use the well-known MAPE-K (Monitor, Analyze, Plane, Execute – Knowledge) feedback loop to realize self-adaptive systems. By extending the Discrete-Event director of Ptolemy, we develop a director that besides an abstract knowledge about the actor-based [email protected] encapsulates the Analyzed and Plan activities of the MAPE-K loop. We use simulation of Ptolemy for the analysis purpose, and augment the director with several adaption policies, e.g. rerouting algorithm in the case of air traffic control systems, for the adaptation purpose. The director is augmented with construction rules to be applied on the actors. For instance, for the case of air traffic control systems, the director prevents two aircraft (two messages) from traveling across the same sub-track at the same time (to be received by the same actor at the same time). We augment our director with predictive adaptation. Upon occurring a change, the director adapts the [email protected] with every adaptation policy, executes the adapted model to calculates performance metrics, compares the results, and based on some criteria, selects the best policy for adaptation purpose. Resources for the predictive adaptation for an air traffic control system are accessible via these links: Paper Source Code

We extend the Discrete-Event director of Ptolemy and develop a nondeterministic model of computation. From a set of actors to be triggered at the same time, the director selects one of them non-deterministically. We use this director to generate the state space of the [email protected] under an adaptation policy and check safety properties, e.g. the fuel of an aircraft does not pass a threshold, the model is deadlock-free, the aircraft arrive at their destinations at the pre-specified times, etc. We develop a Magnifier director that knows the details of each component of the system, e.g. it knows that which aircraft have to flight over which control area, what their arrival times at the components are and what their departure times from the components are. By decomposing the model into several components, Magnifier uses an iterative and incremental process to generate the state space of the model and check the safety properties. Resources for verifying an air traffic control system using Magnifier and the classical state space generation algorithm are accessible via this link: Source Code

More Resources

Project Members

  • Marjan Sirjani (Principal Investigator)
  • Ehsan Khamespanah
  • Maryam Bagheri
  • Ali Jafari
  • Edward A. Lee
  • Narges Khakpour
  • Maryam Bagheri, Marjan Sirjani, Ehsan Khamespanah and Ali Movaghar: Runtime Compositional Verification of Self-adaptive Track-based Traffic Control Systems, Submitted to IEEE Transactions on Software Engineering, Jul 2020 [pdf]

  • 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: Coordinated Actors for Reliable Self-Adaptive Systems, FACS, 2016 [pdf] [bib]

  • 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]