AdaptiveFlow

Problem Description

AdaptiveFlow is a framework that allows to model and analyze track-based flow management systems based on a Eulerian model. In this framework, users provide three input files: environment.xml, topology.xml, and configuration.xml and the Python script will process their content and generates the corresponding Timed Rebeca model for model checking and analysis purposes.

The command for running the Python script is: python ModelGenerator.py envFile topFile confFile outFile. In which envFile is the file that contains information about the configuration of the environment to analyze, topFile specifies the position of Point of Interest, confFile contains information about the machines to simulate, outFile is the file that the script will generate containing the model specification. The so generated model can be run with Timed Rebeca Model Checker for further analysis.

AdaptiveFlow Environment

Python model generator can be found here. Examples of the input files of the system in the figure are: environment.xml, topology.xml, and configuration.xml. An example of a model that violates correctness properties and has a deadlock can be downloaded from here.

More details about this project is provided in this presentation: pptx

Project Members

  • Marjan Sirjani (Principal Investigator)
  • Giorgio Forcina
  • Ali Jafari
  • Ehsan Khamespanah
  • Stephan Baumgart