Tag: verification

Paper Accepted at PNSE 2022

Posted on by bennyakesson

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.

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

Posted on by bennyakesson

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.

Course on Modelling and Analysis of Component-based Systems

Posted on by bennyakesson

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.

Paper Accepted at RTAS 2016

Posted on by bennyakesson

Yonghui Li is on a roll! Two months ago he received the best paper award at ESTIMEDIA for his work on modelling and analysis of a dynamically scheduled DRAM controller using mode-controlled data-flow graphs. Now, he just had a paper entitled “Modeling and Verification of Dynamic Command Scheduling for Real-Time Memory Controllers” that models and analyses the same memory controller using timed atomata. A key highlight of this work is that it quantitatively compares data-flow analysis, timed automata, and two other approaches from Yonghui’s 2015 article in Real-Time Systems in terms of guaranteed bandwidth and worst-case execution time. This gives interesting insights into what these different approaches can and cannot model and what the impact of those limitations are on the performance guarantees. This work was the result of a fruitful collaboration with Kai Lampka from Uppsala University in Sweden.