A PVS Experiment with Asynchronous Communicating Components DRAFT
Jacques Noyé, Jean-Claude Royer · 2004
In our previous work we defined an approach based on symbolic transition system and data type to specify and verify mixed systems. We applied this to components and architectures with full data types, and synchronous communications. However to fit distributed systems, it seems more realistic to consider asynchronous communications. It provides a more primitive communication protocol and maximize the concurrency. To take into account asynchronous communications we distinguish message receipt from message execution and we add mailboxes in our symbolic systems. When we tried to experiment proofs in such a system a difficulty was the presence of buffers and the fact that the receipt instant is distinct from the execution instant. This complicates the specifications and also the proofs. The main problem is that the logic instant to receive is not simply linked with the execution instant. We propose to use an algorithm which decides if the system has bounded mailboxes and computes the reachable mailbox contents of the system. This algorithm gives constraints which are used to specialised the dynamic behaviour of the components according to the current system configuration. Then we are able to generate a PVS specification coping with dynamic behaviour and data type which is simpler since it removes the need for some mailboxes. The component model, the algorithms and the proofs are illustrated on a simple flight system reservation.