Model-based Specification, Verification, and Adaptation of Software Interfaces

As the complexity of cyber-physical systems is increasing, many are thinking about whether a model-based approach to interfaces hold the key to simplifying software decomposition and integration. This raises four important and interesting questions:

1. What does a suitable software interface specification actually look like?

2. How do you verify that a software interface specification is correct?

3. How do you verify that interactions between components always work correctly?

4. How do we ensure that component interactions continue to work correctly as the software is continuously evolving?

Last year, I rounded off an applied research project called DYNAMICS, a public/private collaboration between ESI (TNO) and Thales. This concluded a three-year effort in the area of specification, verification, and adaptation of software interfaces that had been running between 2019 and 2021. In this blog post, I try to answer the four questions stated above based on the results from this project. First, I will briefly elaborate on the complexity of cyber-physical systems and the problem we were challenged with. I will then present the six-step methodology we developed to address that challenge, summarize the key results of the project in the context of the ESI mission, and briefly look at how the work was received and the impact it has created so far.

Nearly all problems addressed in ESI projects can be traced back to the increasing complexity of cyber-physical systems. It does not seem to matter much what the particular application domain is, the complexity is increasing because of a few common technological and market drivers.
Three complexity drivers relevant to this story are:

1. Systems integrate an increasing amount of functionality, often implemented in software, resulting in software-intensive cyber-physical systems where the number of interfaces and lines of code are increasing by an order of magnitude.

2. There is an increasing trend towards mass customization of systems, a trend that is going from a few variants within a product line towards each delivered system being unique in some aspect.

3. Cyber-physical systems may have long life-times and need to continuously evolve after deployment to enable safe and secure operation, as well as deliver increased value to the customer through new functionality.

Modularity is often used to manage the increasing complexity of cyber-physical systems, as it enables us to divide the system into smaller pieces with clear responsibilities, allowing complexity to be managed through a divide-and-conquer approach, both in terms of function and ownership within an organization. In software, this is typically achieved by using component-based software architectures, where components request and provide services corresponding to particular functionality. These services are described through interfaces that abstract the implementation of the service and only describe its externally visible characteristics. This abstraction makes the implementing component, as well as the implementation technology, transparent, allowing them to be changed in a plug and play manner, which make them easier to customize and evolve. Components communicate through message passing, which is often asynchronous, to achieve low coupling between components.

Component-based architectures clearly help mitigate the three complexity drivers mentioned above and are common in well-known companies in the Dutch High-tech industry. However, these architectures still face two important challenges that we addressed in the project:

1. Component-based software architectures result in systems that are highly concurrent, loosely coupled systems, which leads to an explosion of possible behaviors. This makes the system behavior hard to verify, resulting in that early design errors are detected much later in the system life-cycle when the cost and effort required to address them is much higher.

2. The cost of updating interfaces becomes prohibitive. When an interface changes, the abstraction it provides for the implementing components breaks, requiring all of them to be updated. Although updating the interface itself may be done quickly, updating and verifying many incompatible components is expensive and time consuming. This results in reluctance to update interfaces, resulting in creative workarounds and accumulation of technical debt.

The mission of ESI is to embed cutting-edge methodologies into the Dutch high-tech systems industry in order to cope with the ever-increasing complexity of their products. In that sense, it may not be surprising that the key outcome of this project is a methodology, shown in Figure 1. We will briefly describe the six steps of the methodology below.

1. The structure and behavior (in terms of a protocol state machine) of server and client interfaces are formally specified using Eclipse ComMASuite. A part of such an interface is shown in Figure 2. The interface specification may be baseline versions of the client and server interfaces, or updates of the interfaces as they evolve. These formalized specifications enable a model-based approach to address the complexity challenge and provides the option to generate documentation, visualizations, simulation models, conformance monitors, and test cases from the interface specifications. This provides the answer to the first question in the introduction of this blog post.

2.The quality of each of the specified interfaces is independently verified by transforming them to a Petri net representation and using reachability analysis to detect problems in the protocol state machine. Specification problems, such as unreachable states, deadlocks, livelocks, and sink states, are detected in this way. This answers the second question from the introduction for a particular definition of correctness. Note that Eclipse CommaSuite can also verify other aspects of correctness, e.g. whether an implementation corresponds to the specification using compliance monitoring.

3. The Petri net representation is also used to verify interaction problems, such as race conditions or confusion with a general class of clients. Problems are presented on a dashboard along with design guidelines for how to resolve them. This is shown in Figure 3. In addition, the structural and behavioral compatibility between the particular server and client interface is verified to ensure they fit together and that their interactions do not cause deadlock, livelock, or unbounded memory behavior. If they are compatible, no further steps in the methodology are needed. This answers the third question from the introduction.

4. If there is an incompatibility, an adapter between the client and server can be specified using a Mapping DSL, an extension to Eclipse ComMASuite, which states how messages from one interface maps to the other. This may involve splitting up and merging certain messages, but also automatic creation of messages that are required in a new version of an interface, or deletion of messages that are no longer necessary.

5. The compatibility between the server and client is formally verified again when connected through a generated Petri net model of an adapter that implements the specified mapping. If compatibility problems persist, the mapping can be modified and a new adapter model generated.

6. Once the client and server are finally compatible, an implementation of the specified adapter is generated is deployed in the software platform. For ease of experimentation, in our prototype, the adapter was always present in the software platform, but could be programmed with different adapter models. Together, Steps 4-6 answer the fourth and last question from the introduction.

This methodology leveraged open source software from the ESI eco-system (Eclipse ComMASuite) in which years of investment had been done together with other ESI partners. At the end of the project, the DYNAMICS project contributed new functionality, ComMA interface verification, to Eclipse ComMASuite, allowing others to benefit from the work done in the project. This is an example of open innovation in the ESI eco-system. Partners should get a multiplier on their investment through the eco-system; they should get out more than they put in because they are better and stronger together!

While the methodology for specification, verification, and adaptation of software interfaces, detailed above, is clearly a key result of the project, a methodology alone cannot fulfill the ESI mission. To make a methodology concrete and applicable to practical problems, it often needs to be supported by an implementation. In this case, a prototype of the proposed methodology was created on Thales software platform. The methodology and prototype implementation were validated through application to two Thales case studies, allowing them to validated in the context of an industrial platform and industrial problems, a key requirement for applied research and a differentiator with fundamental academic research.

The ESI mission, stated above, emphasizes that it is not just about inventing new methodologies, but also embedding them in organizations. For this reason, much of the knowledge generated in the project has been consolidated in a course “Modelling and Analysis of Component-based Systems” (MOANA-CBS) that exists in two versions, one for academia and one for industry, respectively. The academic version teaches the principles of interface specification and verification in a technology-agnostic way using Petri nets, while the industry version is based on Eclipse ComMASuite to make it easier to transfer the acquired knowledge to the workplace. Together, the two versions of the course have been given eight times to a total of approximately 150 participants. More instances of both versions of the course are planned in the near future.

 Like most other research projects, there was also consolidation and dissemination of project results through publications and presentations. Project results were disseminated through six publications, out of which three are academic papers, two are bachelor and master theses, and one is an article in the trade press (see list of publications below). There were also 16 project presentations to a variety of stakeholders that were attended by 300+ participants in total. Lastly, five presentations from related ESI projects were facilitated at Thales and were attended in total by more than 150 participants. This is another example of cross-fertilization between projects in the ESI eco-system, allowing partners to share and learn from each other.

While the results of a research project are available when it ends, it takes time, often years in my experience, to determine the impact it had on the participating organizations, the scientific community, and society. For the DYNAMICS project, this process has only started. The project results have been transferred to Thales and are being evaluated for use within the company. In particular, Eclipse ComMASuite is being internally evaluated as technology for specification of interfaces in different parts of the organization. In addition, Thales has trained two trainers for the MOANA-CBS course and they have already taught the course internally by themselves, with more sessions planned in the future. This is an important milestone, because it means the knowledge we developed together in the project has been sustainably transferred to the industry partner.

The project received a full score, 5 out of 5 possible, from Thales in TNO’s customer satisfaction survey. Although this shows great appreciation of the work we did together in the project, the most satisfying recognition, in my opinion, is that we are already working together in a new project. Nothing is more valuable than the long-term strategic relations we build with the partners in the ESI eco-system.

If you found this blog post interesting and want to learn more, have a look at the publications listed below or download and experiment with Eclipse ComMASuite to see how it fits your needs. If you are interested in a training that introduces interface specification and verification with Eclipse ComMASuite, contact us about participation in the

Academic Publications

• Partial Specifications of Component-based Systems using Petri Nets
  Bart-Jan Hilbrands, Debjyoti Bera, and Benny Akesson
  In: International Workshop on Petri Nets and Software Engineering, 2022 

• Synthetic Portnet Generation with Controllable Complexity for Testing and Benchmarking
  Madiou Diallo, Benny Akesson, Debjyoti Bera, and Ronald Begeer
  In: International Workshop on Petri Nets and Software Engineering, 2021 

• Towards Continuous Evolution through Automatic Detection and Correction of Service Incompatibilities
  Benny Akesson, Jack Sleuters, Sven Weiss, and Ronald Begeer
  In: International Workshop on Interplay of Model-driven and Component-based Software Engineering, 2019

Theses

• Verification of Inter-dependent Interfaces in Component-based Architectures
  Bart-Jan Hilbrands, Master thesis, University of Amsterdam 2021

• Towards the Scalability of Detecting and Correcting Incompatible Service Interfaces
  Madiou Diallo, Bachelor thesis, University of Amsterdam, 2020

Trade Press

•  ComMA interfaces open the door to reliable high-tech systems, Bits & Chips, September 2020