Reachability Analysis of Hybrid Rebeca Models
Formal Methods and Validation of Systems Lab, University of Tehran
I worked on implementing Hybrid Rebeca, an extension of the Rebeca programming language, designed for modeling asynchronous event-based cyber-physical systems with non-deterministic time behavior, under the supervision of Prof. F. Ghassemi.
My responsibilities included developing an efficient reachability analysis technique to ensure the correctness of the models created in this language, as well as detecting program vulnerabilities, inappropriate software states, and potential bugs.
You can find the code and other material on the GitHub repository.