Merrick Oost-Rosengren Successfully Defends Thesis on Early Component Verification using Colored Petri Nets

Just before the summer holidays, another master student has finished his project. This time, it is Merrick Oost-Rosengren who successfully defended his thesis “Formal Verification of Components through Mirroring of Coloured Petri Nets“. Parts of this work was done as an internship with TNO-ESI in collaboration with Thales.

This research addresses a challenge in distributed component-based systems, where different components are developed by different teams, perhaps even different organizations, over time. The problem is that when components are ultimately integrated, their interactions may cause deadlocks, livelock, or unbounded memory behavior. Fixing such problems late in the development process is very costly. An alternative approach is to model components, or component interfaces, early in the design process and use model checking to verify the behavior of the component and its interactions. However, we may not know which components it will interact with yet. Perhaps they have not yet been developed?

The thesis addresses this challenge by proposing a methodology and corresponding tool chain, where components as modelled as Colored Petri Nets from which a verification model, a mirror of the component that captures relevant possible behaviors of interacting components, is automatically generated. As a part of the methodology, the thesis proposes a new class of Colored Petri Nets called Mirrorable Open Colored Petri Nets. This class combines features of existing Colored Petri Nets and Open Petri Nets, and also adds extra semantics to allow the component to be mirrored. It also describes methods for mirroring such a net and fusing the mirror with the original component, such that the components and its interactions can be verified using reachability analysis.

We congratulate Merrick on his successful defense and wish him a lovely summer!

Specification, Verification, and Adaptation of Software Interfaces using Eclipse ComMASuite

Software interfaces are key to realizing the benefits of component-based software architectures, yet specifying interfaces is difficult and may result in problems in the protocol specification itself, or in its interactions with clients. This problem is addressed through a six-step methodology for specification, verification, and adaptation of software interfaces. The methodology builds on the open-source tool Eclipse ComMASuite, developed by TNO-ESI partners in an open innovation eco-system. The specification and verification steps have been contributed back to the community and are supported by a two-day course named “Modelling and Analysis of Component-based Systems”, available from TNO-ESI in both an academic and industry version.

Please read my blog post that describes the methodology and demonstrates it step-by-step from a user perspective through a simple case study in a video.

Paper Accepted at PNSE 2022

I am happy to announce that the paper “Partial Specifications of Component-based Systems using Petri Nets” has been accepted for publication at the International Workshop on Petri Nets and Software Engineering (PNSE) 2022. This paper was first-authored by Bart-Jan Hilbrands, a (former) student in the Master of Software Engineering program at the University of Amsterdam, who did his master thesis project under the supervision of myself and my ESI colleague Debjyoti Bera. The master thesis project was conducted in the context of the DYNAMICS project, a bi-lateral research project between ESI and Thales, which looked into specification, verification, and adaptation of software interfaces.  This publication is a good example of how a good master thesis can be turned into a publication.

The paper addresses the problem of verifying correctness properties, such as absence of deadlocks, livelocks, and buffer overflows, in software components with multiple inter-dependent interfaces. An approach based on partial specification of dependencies between interfaces, expressed as a set of functional constraints, is proposed in the paper. The papers presents and formalizes three commonly occurring functional constraints and provides algorithms for encoding them into a Petri net representation of the interfaces, enabling interface verification through reachability analysis. The approach has been implemented and demonstrated using ComMA.

Seven Brave Software Architects/Engineers from Thales Completes MOANA-CBS Course using Eclipse ComMASuite

ESI (TNO) has given another instance of the course “Modelling and Analysis of Component-based Systems” (MOANA-CBS), developed as part of the applied research project DYNAMICS, at Thales. A batch of 7 brave software engineers participated to learn more about how to identify and resolve a range of interface model quality problems, such as deadlocks, livelocks, and race conditions. This instance of the course was adapted to be based completely on the latest version of Eclipse ComMASuite, the open source version of ComMA, making the course accessible to a large general audience. Previously, the course has been given with an internal version of ComMA or by using Petri nets as the interface modelling language.

 In total, over 110 participants, mostly with backgrounds in system and software engineering, have followed different versions of this course. This time, two former Thales participants assisted in giving the course, both by presenting contents and supervising exercises, to help Thales transfer the knowledge developed in the DYNAMICS project into the organization. We look forward to further improve the material and keep sharing the knowledge we developed with Thales and other interested parties.

Modelling and Analysis of Component-based Systems (MOANA-CBS) Course Update

Last year, ESI (TNO) and Thales developed a two-day course on Modelling and Analysis of Component-based Systems (MOANA-CBS) as a part of the DYNAMICS project. The course addresses the trend to tackle software complexity by decomposing monolithic software into loosely coupled components. While this trend manages complexity through improved scalability, adaptability, and testability, it also increases concurrency and asynchronous communication. This may in turn lead to an explosion in possible behaviors. As a consequence, it is hard to oversee the behavior of such systems, resulting in situations where early design errors are detected much later in the system lifecycle with exponentially rising costs. The course targets software and system architects/engineers involved in design and implementation of components and interfaces, and teaches methods for modelling and analyzing them to guarantee that they are free from deadlocks, livelocks, races, and buffer overflows.

We piloted the course material both in academic and industrial environments. The former was as a part of my course Embedded Software and Systems, a part of the Software Engineering Master  at the University of Amsterdam. The latter was as a part of the Accelerate program run by Thales and Luminis to accelerate their medior software talent to a senior level. Thales recently published an interview with Patrick Schulenberg, one of the participants in the program, about his experience. Patrick explains that the program has been an excellent opportunity for him to grow within the company, and mentions the positive impact of our course: “ESI taught a class about interface modeling, sharing their experiences with using the Comma framework at Philips – this was a trigger for us to put practical modeling proficiency on our roadmap”.

Currently, we are developing an updated version of the MOANA-CBS course that will have closer ties to ComMA, an open-source domain-specific language initially developed by Philips and ESI that is currently used by several companies. This update will strengthen the practical applicability of the course for users of ComMA, and will introduce unfamiliar users to interface modelling and analysis through hands-on experience with the tool. The new version of the course is expected to be ready in Q3.

Paper Accepted at PNSE 2021

It has been almost a year since Mohammed (Madiou) Diallo submitted his bachelor thesis “Towards the Scalability of Detecting and Correcting Incompatible Service Interfaces“, which he carried out in the context of the DYNAMICS project, an applied research project between ESI (TNO) and Thales. After the thesis was finished, we discussed publishing the work as a paper and one year later, a slightly restructured and simplified version of the story has been accepted at the International Workshop on Petri Nets and Software Engineering (PNSE), a workshop co-located with the Petri Net conference.

The accepted paper is entitled “Synthetic Portnet Generation with Controllable Complexity for Testing and Benchmarking” and presents a heuristic-driven method for synthetic generation of random portnets, a kind of Petri Nets suitable for modelling software interfaces in component-based systems. The method considers three user-specified complexity parameters: the expected number input and output places, and the prevalence of non-determinism in the skeleton of the generated net. An implementation of this method is available as an open-source Python tool. Experiments demonstrate the relations between the three complexity parameters and investigate the boundaries of the proposed method. This work was helpful for the DYNAMICS project, as it allowed us to synthetically generate a large number of interfaces of varying complexity that we could use to evaluate the scalability of existing academic tools for adapter generation.

 

 

Open-source ComMA v0.1.0 officially released

Last week, the open sourcing of ComMA (Component Modelling and Analysis) in the context of the Eclipse Foundation, saw another milestone. The first version Eclipse CommaSuite is now online in the form of Release 0.1.0. ComMA is a set of DSLs used to (partially) specify the behavior of components and their interfaces, including time and data constraints. On the basis of these specifications, a number of artifacts can be automatically generated, including run-time monitors that validate compliance with the specification can be generated, visualizations, timing statistics, documentation, test cases, and adapters. Many of these features will be included in later releases of ComMA, and some of them have yet to emerge from research projects as mature features.

ComMA was originally developed by ESI and Philips, but more recently in collaboration with a growing number of other companies. For example, the DYNAMICS project in which ESI works together with Thales, we are currently investigating how adapters can be semi-automatically generated to bridge differences between components implementing different versions of interfaces. This work has been previously mentioned in an article in Bits & Chips, as well as in a paper. Currently, three master students from my Embedded Software and Systems course at UvA are also doing their graduation projects in the context of evolution of ComMA interfaces, looking into aspects of data dependencies, interface dependencies, and static impact analysis. We look forward to seeing the results of their work this summer.

You can read more about ComMA in this news article TNO published this week.
Update: The news article is now also published in Bits & Chips

Model-based Engineering Dominates Software-Centric Systems Conference

I attended the online edition of Software-Centric Systems Conference (SC2) today. Although I prefer the networking and social aspects of a physical conference, it was nice to enjoy these presentations from the comfort of my couch.

It was interesting to see that most of the conference presentations were related to domain-specific languages (DSLs) in one way or another. There were also presentations about model-based testing and digital twinning. I am not sure if model-based engineering was an intentional theme, or if this is just what is considered interesting in software-centric systems in the Netherlands for the moment. However, this suggests that the applied research into model-based design methodologies done by ESI (TNO) together with its industrial eco-system is highly relevant.

A highlight for myself was the two presentations about the Component Modelling and Analysis (ComMA) DSL. This is not only because it relates to my research on evolvable interfaces, but also because of the main message that the industry can achieve a lot through open innovation in areas that are not their core business, such as specification, verification, and evolution of software interfaces. Great news that ComMA will become open-source in 2021!

DYNAMICS Project in Keynote at Software-Centric Systems Conference

Two months ago, I mentioned that Bits & Chips had published an article about the ComMA (Component Modelling and Analysis) language and how it is being used in Philips and Thales to address challenges related to integration and evolution. The latter part, about semi-automatic detection and correction of interface incompatibilities as interfaces evolve is the topic of the DYNAMICS project, a research project between ESI (TNO) and Thales. This joint story, where two companies from different domains together presented their challenges and how it was addressed by technology developed by ESI was much appreciated by Bits & Chips and was invited as a keynote at the Software-Centric Systems Conference (SC2), which takes place on Thursday November 5. If you are interested in hearing this keynote, please register for the event. All presentations are also available on-demand after the event in case you cannot attend in real time.

Course on Modelling and Analysis of Component-based Systems

A course called “Modelling and Analysis of Component-based Systems” (MOANA-CBS) is being developed in collaboration with Thales as a part of the DYNAMICS project. The course addresses the challenge of overseeing the explosion of possible interactions between asynchronously communicating components in component-based systems. Some of these interactions may be undesirable and leave systems prone to deadlock, livelock, race conditions, and buffer overflows, reducing software quality. The course participants in the course learn how to mitigate this problem by modelling the behavior of components and interfaces using Petri Nets, a well-known formalism suitable for describing asynchronously communicating systems. Theory is linked to practice through demonstrations of relevant examples using the ComMA tool. Using properties and analysis methods for Petri Nets, they learn how to identify patterns in component and interface design that may cause the aforementioned problems, as well as design guidelines for how to avoid them. The course is taught using a combination of lectures, assignments, demonstrations, discussions, and reflection.

We piloted parts of the course at Van der Valk Hotel in Arnhem on October 7 and 8, attended by 12 software architects from Thales and Luminis. The course was positioned as a part of their Accelerate program, which aims to accelerate young architects from the two companies into a more senior role. We felt that the delivery of the course went well and evaluations from the participants suggests it was well-received. The evaluation of this pilot also highlighted some further points for improvement that will be considered going forward.