verification

Our research group has presented the Gamma framework at the Modeling Symposium of EclipseCon 2017. Gamma is a Statechart Composition Framework to model, verify and generate code for component-based reactive systems. The framework builds on Yakindu, an open source statechart modeling tool and provides an additional modeling layer to instatiate a communicating network of statecharts. Compositionality is hierarchical, which facilitates the creation of reusable component libraries.

Our paper entitled "New search strategies for the Petri net CEGAR approach" is accepted to the "36th International Conference on Application and Theory of Petri Nets and Concurrency".

This paper introduces our theoretical and algorithmic results regarding the advanced CounterExample Guided Abstraction Refinement algorithm applied to Petri nets.

A paper by our research group has been accepted at the TACAS 2015 (International Conference on Tools and Algorithms for the Construction and Analysis of Systems) scientific conference, a top international forum for tools and algorithms for the construction and analysis of systems.

We would like to thank our student collaborators and the reviewers for their helpful feedback.

The title of our accepted paper: Saturation-based Incremental LTL Model Checking with Inductive Proofs

Next laboratory (on Tuesday, 12. October 2013) will be about formal modelling.

Please download UPPAAL tool (http://www.uppaal.org/) which is free for academic use and bring it to the next lesson (if possible).

Please read the short introduction! You can find it in the Course materials: https://www.inf.mit.bme.hu/en/edu/courses/materials/critical-embedded-sy...

The summer workshop of the IFIP WG10.4 "Dependable Computing and Fault Tolerance" working group was held at Visegrád between June 27-30, organized by Prof. András Pataricza.  István Majzik received an invitation to the workshop and gave a presentation on "Testing the Robustness and Safety of Context-Aware Autonomous Behaviour". Read more »