To build dependable systems we need to be able to have different techniques for thorough analysis. There is a wide range of analysis techniques, including testing, simulation, assertion check, light weight formal verification and statistical model checking. Building different models of the system, in various levels of abstraction, helps in managing the complexity of analyzing cyber physical systems and systems of systems. It also helps in managing any change in the architecture design. More abstract models can better show how any change in one component may have a propagating effect in other components.
We will focus on modeling and analyzing event-based asynchronous autonomous systems for safety assurance, performance evaluation, and optimization. Based on the application we may focus on planning, scheduling or routing.
The domain can be collaborating autonomous machines, collaborating agents, or event-based distributed programs executing on different network nodes to accomplish a certain goal.
Here we choose two platforms, Rebeca and Ptolemy, which both target distributed and concurrent systems, and can model timing constraints. Rebeca tools can check assertions and deadline misses, while Ptolemy shows the architecture and is supported by a powerful and visual simulation tool. Both tools provide performance evaluation using different techniques, Rebeca can model uncertainties using probabilities and Ptolemy uses traditional simulation techniques. This makes it possible to explore the design space to make better design decisions.
Overall project description: Modeling and analyzing collaborating autonomous systems (or distributed agents), considering the computation time and costs (like energy consumption), and different communication patterns and protocols, in order to check safety properties and evaluate performance, and suggesting and investigating different heuristics for optimization.
There are different types of computation with different level of criticality and priority. There are also different communication types, for example in automotive industry we have communication within a car, between two cars, and via cloud (where the third type is usually not time critical) and primarily with packet-based protocols to optimize flexibility and bandwidth. An example is when a car gets too close to another car, this has to be captured by a sensor (communication between two cars), and then a command has to be sent to Brake (communication within a car). There are other constraints, like the bandwidth, power and the flexibility/robustness for communication/interface updates. The goal is to find out the optimum solution.
|Associated Senior Lecturer
|Industrial Doctoral Student
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)
From Requirements to Verifiable Executable Models using Rebeca (Sep 2020) Marjan Sirjani, Luciana Provenzano, Sara Abbaspour, Mahshid Helali Moghadam Software Engineering and Formal Methods Collocated Workshops 2020 (SEFMW 2020)
An Actor-based Approach for Security Analysis of Cyber-Physical Systems (Sep 2020) Fereidoun Moradi, Sara Abbaspour, Ali Sedaghatbaf, Aida Causevic, Marjan Sirjani, Carolyn Talcott 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS20)
Model Checking Software in Cyberphysical Systems (Jul 2020) Marjan Sirjani, Edward Lee, Ehsan Khamespanah 44th Annual Computers, Software, and Applications Conference (COMPSAC 2020)
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)