Rebeca for Actor Analysis in Action
Description
This Festschrift volume, dedicated to Marjan Sirjani on the occasion of her 60th birthday, includes refereed papers by leading researchers.
Marjan Sirjani received her PhD in Computer Engineering from Sharif University of Technology for work on the Formal Specification and Verification of Concurrent and Reactive Systems. After Postdoc, Lecturer, Visiting Scholar, Associate Professor, and Professor positions in Iran, The Netherlands, Iceland, and the US, she has been a Professor in the School of Innovation, Design and Engineering of Mälardalen University since 2016. Her main fields of interest are Software Engineering, Formal Methods, Cyber-Physical Systems Analysis, Model Checking, Distributed Systems, and Applying Formal Methods in System Design. Among other successes, Marjan invented the Rebeca modelling language, one of the best-known actor-based languages with a formal semantics and a wealth of analysis and verification tools. Rebeca has been used in modelling and analysis of a wide range of systems, including in domains such as biomedical engineering, automotive, and aviation.
Throughout her career, Marjan has trained many students and worked successfully with a range of scientists and engineers across disciplines, these collaborations are reflected in the papers in this volume.
More details
Other editions
Additional editions
Content
-. Modelling Cyber-Physical Systems for Verification and Synthesis.
-. 20 Years of Actor Model Checking with Rebeca - From Dining Philosophers to MicroServices. Responsibility in Actor-Based Systems.
-. Semantics and Formal Analysis of Lingua Franca CPS Specifications in Rewriting Logic.
-. Parallel Composition of Constraint Automata.
-. Privacy-Aware Modeling and Analysis of Social Networks Using Rebeca Ranch: Rebeca on Chip Animating Rebeca.
-. Verify Engineering Models, not Scientific Models.
-. Black-box protocol testing using Rebeca and Automata Learning.
-. From LTL to Scenarios: Automatic test case generation for Axini Modeling Language.
-. Concurrent Rules Machines Verifying ROS Systems Using Timed and Stochastic Timed Automata.
-. An LAGC Semantics for Timed Rebeca Inside Every Multi-Threaded Program There Are Active Objects Struggling To Get Out.
-. A Debugging System for Language-parameterized Proofs Security Threats and Challenges of Digital Twins-enabled Self-adaptive Systems.
-. Ten Years of Spatial Model Checking.