The FCPP AP framework (Monday, 20 Jun) | Model-based SE for/with PNs (Tue, 21 Jun)
Date: Monday, 20 June 2022
Time: 14:00–17:30
Room: M005
As the density of computing devices in human environments continues to increase, the costs and challenges of maintaining distributed systems rise, driving a search for solutions increasing the autonomy of computing systems while reducing their overall complexity. Aggregate Programming (AP) is an emerging macro-programming approach, aiming at the abstraction of a network as a single spatially distributed and inherently robust platform to be programmed as a whole. This approach allows the functional composition of reusable blocks of collective behaviour, simplifying the study of resilience properties for distributed behaviour, such as: self-stabilisation, density independence, and runtime verification of formulas in spatio-temporal logics.
Among other tools for programming and simulating distributed systems, the FCPP library stands out for its efficiency, portability and extensibility, and its support for aggregate programs. The library enables both deployments on networks of microcontrollers and simulations thereof, through a unified framework in which a distributed program can first be tested in simulation, and then concretely deployed. The simulator supports both batch collection of numeric statistical information, across multiple randomised executions of the distributed systems, as well as a real-time, interactive and three-dimensional visualization of the simulated system. Through a graphical user interface, the user can control the simulation flow, visualize summary information of the network at a single glance, and inspect detailed information via auxiliary windows. The interface is designed to require minimal effort from the end user for its setup, and can be further extended for increased interaction.
This tutorial presents the idea and main concepts of Aggregate Programming and spatio-temporal runtime verification, with a hands-on approach based on FCPP. We will run some existing examples, then we will customise them to get further insight in their inner workings. These examples will include archetypal routines in distributed systems (e.g, routing, data collection, leader election), as well as automated checking of spatio-temporal formulas. In order to follow the tutorial, you will need your own laptop, the GCC or CLANG compilers, CMake, and possibly other dependencies that may differ based on your operating system. It is strongly advised to install the needed software beforehand, as detailed in: https://github.com/fcpp/fcpp-exercises#setup. A recorded walkthrough is also available at: https://www.youtube.com/watch?v=zWsNqJMVxKs.
Date: Tuesday, 21 June 2022
Time: 09:00–17:30
Room: M005
Model-based Software Engineering (MBSE) is a catch-all term for software development technologies in which models are more than just “nice sketches” or “drawings”. In MBSE, models are mostly used for generating some parts of the code automatically from models or for executing models directly. The OMG’s Model Driven Architecture (MDA) is probably one of the most prominent approaches in this direction and Eclipse EMF is a very popular technology supporting MBSE. But, MBSE also covers approaches that are more focussed on analysing or verifying software models.
Petri nets have been used for modelling for a long time now and they are successfully used in different areas of software and systems development. Though Petri nets are used in all stages of software development, many approaches focus on the early phases of the development process and for building prototypes; the actual software is often still programmed manually.
This tutorial present the idea, the main concepts, and some technologies of MBSE — with the focus on automatic code generation. On the one hand, these technologies can be used for developing Petri net tools in a more efficient way. On the other hand, they can be used to generate parts of the software automatically from Petri net models. More importantly, we will see how Petri nets and the code generated from them can be integrated with other software.
This tutorial will be based on the experiences with Eclipse EMF and developing the ePNK based on EMF, and discuss the lessons learned with developing the ECNO Tool, which allows to generate software completely automatically from models which consists of the Event Coordination Notation and ECNO nets (which are a special version of Petri nets for modelling the life-cycle of is components).