You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.
The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.
For the reports in this repository we specifically note that
By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.
If you are in doubt, feel free to contact email@example.com
The good old days of computation when we abstracted away time and uncertainty are passed. In this new era of Cyber-Physical systems, we have to address timeliness and probability as main features in our models. To explore the design space, and to analyse safety and performance of models efficiently and effectively we need usable and analysable models. Probabilistic Timed Rebeca is introduced to enable model driven development and bridge the gap between formal methods and software engineering. The language is actor-based which makes it natural for building distributed, asynchronous, and event-based systems. Model checking and simulation tools are developed to support formal verification and performance evaluation. In this talk I will explain Rebeca together with the timed and probabilistic extensions of it, and show how it can be used in model driven development using a Network on Chip example.
Marjan Sirjani is a Professor at School of Computer Science at Reykjavik University. Her main research interest is applying formal methods in Software Engineering. She works on modeling and verification of concurrent and distributed systems.
Marjan and her research group are pioneers in building model checking tools, compositional verification theories, and state-space reduction techniques for actor-based models. She has been working on analyzing actors since 2001 using the modeling language Rebeca (www.rebeca-lang.org ). Rebeca and its extensions are designed to bridge the gap between model-based software development and formal analysis, and has been used for analyzing different network and system applications. She has also worked on coordination languages and is the co-author of the paper proposing Constraint Automata as the compositional formal semantics for the coordination language Reo. Marjan has been the PC member and PC chair of several international conferences including Coordination, FM, FMICS, ICFEM, FSEN, and guest editor for special issues of the journals Science of Computer Programming and Fundamenta Informaticae. Before joining academia as a full-time faculty she has been the managing director of Behin System Company for more than ten years, developing software and providing system services. Marjan served as the head of the Software Engineering Department of School of Electrical and Computer Engineering at the University of Tehran prior to joining the School of Computer Science at Reykjavik University in 2008.