Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4951420 | Journal of Logical and Algebraic Methods in Programming | 2017 | 40 Pages |
Abstract
Components also provide a convenient abstraction for verifying the correct behaviour of systems: they provide structuring entities easing the correctness verification. This article provides a formal background for the generation of behavioural semantics for asynchronous components. It expresses the semantics of hierarchical distributed components communicating asynchronously by requests, futures, and replies; this semantics is provided using the pNet intermediate language. This article both demonstrates the expressiveness of the pNet model and formally specifies the complete process of the generation of a behavioural model for a distributed component system. The purpose of our behavioural semantics is to allow for verification both by finite instantiation and model-checking, and by techniques for infinite systems.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
R. Ameur-Boulifa, L. Henrio, O. Kulankhina, E. Madelaine, A. Savu,