Verification of Asynchronous Systems with an Unspecified Component

TL;DR

This paper presents a method for verifying safety properties of asynchronous component-based systems with unspecified components by generating assumptions and overapproximated interfaces, enabling modular verification and reducing complexity.

Contribution

It introduces an assume-guarantee reasoning approach tailored for asynchronous systems with unspecified components, improving verification efficiency and assumption precision.

Findings

Assumptions generated are smaller than existing methods.

Verification process is faster and more scalable.

Approach successfully applied to case studies.

Abstract

Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may result in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. To this aim, we study the problem of model checking component-based asynchronously communicating systems in the presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous environments, which generates the weakest assumption. If the newly added component conforms to the assumption, then the whole system still satisfies the property. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by its composition with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property and generate an assumption for the missing component. We have implemented our approach on two case studies. Furthermore, we compared our results with the state of the art direct approach. Our resulting assumptions are smaller in size and achieved faster.