Verification of Concurrent Systems in a Model-Driven Engineering Workflow

Concurrent systems form an integral part of today’s society. From smartphones, desktops and web systems to the car you drive, and even your coffee machine, concurrent systems can be found everywhere. Concurrency in systems has many benefits; e.g. better performance, better distribution of services. However, due to their non-deterministic nature concurrent systems are also more complex, harder to understand, and harder to develop than sequential programs. Researchers and practitioners have sought to alleviate complexity, increase understandability, and facilitate the early and automated detection of faults. To this end, formal methods and Model-Driven Engineering (MDE) are widely applied. In this thesis, we investigate automated formal methods to determine and guarantee correctness of concurrent systems and the integration of formal methods with MDE.

A popular method for verify the functional correctness of concurrent systems is model-checking. In model-checking a model, representing of the concurrent system, is verified against a number of formal requirements. With the model verified, one expects that the corresponding implementation will also meets the requirements. Yet there are several significant problems to cover.

First, if the implementation does not formally adhere to the specification all guarantees are void. The closer the model serving as specification is to the actual implementation, the more confidence one has in the correctness of the implementation. To bridge the gap between specification and implementation a series of transformations can be applied adding the required details. These transformations have to be verified as well. Nonetheless, verification of model transformations is still in its infancy. In this thesis we propose a formal verification technique to determine that formalisations of such transformations in the form of rule systems are guaranteed to preserve functional properties.

Second, another problem arises when the model becomes too detailed called the state space explosion problem. The state space that the verification considers is exponential in the size of the individual components and the number of parallel components. To reduce the state space explosion, many technique make use of Divergence Preserving Branching Bisimulation (DPBB) to reduce size of the state space. This is only correct if DPBB is a congruence for parallel composition with synchronisation. This thesis finally proves that this is indeed the case.

Third, to further limit state space explosion, several approaches have been proposed that reason compositionally about concurrent systems. One such approach, called compositional aggregation, which has shown to perform better (in the size of the largest state space in memory at one time) than classical monolithic composition in a number of cases. Still, it is unclear when one should apply compositional aggregation in favour of other techniques and how it is affected by action hiding and the scale of the model. This thesis presents a descriptive analysis following the quantitative experimental approach and apply machine learning techniques to predict which of three compositional strategies performs best in terms of maximum memory cost. The learned prediction models achieved an accuracy between 55% and 61% on unseen data.

Fourth, even when code is generated from the verified model, bugs may still occur due to the interleaving of parallel execution of the components. Software developers expect their executions of their programs to be Sequentially Consistent (SC), i.e., the program executes in sequential order and atomic behaviour is not interrupted. Violations of sequential consistency are a major source of bugs. Static analysis techniques can be used to insert synchronisation mechanisms that guarantee that program executions are indistinguishable SC ones. Alternatively, executions can be monitored and violations can be reported at run-time. While the first approach is more efficient (no run-time monitoring is required), the second approach is more precise. In this thesis we combine the two approaches into an efficient monitor for model checkers.

Finally, we combine our results in an framework supporting verification various aspects of the MDE workflow.