Verificación de procesos concurrentes: un método formal y un caso de aplicación
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2099/4375
Tipus de documentArticle
Data publicació1980-09
EditorUniversitat Politècnica de Barcelona. Centre de Càlcul
Condicions d'accésAccés obert
Llevat que s'hi indiqui el contrari, els
continguts d'aquesta obra estan subjectes a la llicència de Creative Commons
:
Reconeixement-NoComercial-SenseObraDerivada 2.5 Espanya
Abstract
En este trabajo se propone una nueva tècnica para la verificación de programas concurrentes. Para realizar la verificación se parte de la descripción LDP de los procesos.
El método requiere expresar en una relación de simulación las prioridades que se desea probar. El algoritmo de verificación construye mediante ejecución simbólica un árbol de prueba para cada punto de paro de la relación de simulación. La verificación se reduce así a la prueba de las condiciones de verificación generadas.
Como caso de aplicación se presenta la verificación de un conocido protocolo de comunicación: el protocolo de bit alternante. In this work a new technique for verifying concurrent processes is presented. The LDP specifications of the processes serve as the basis for the verification.
The properties the designer wants to prove must be expressed through a simulation relation, and the verification algorithm generates, by means of symbolic execution, a proof tree for every stopping point of the simulation relation. Verification is thus reduced to the proof of the generated verification conditions.
As a particular case the verification of a well known communication protocol –the alternating bit protocol- is discussed.
ISSN0210-8054 (versió paper)
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
article.pdf | 657,5Kb | Visualitza/Obre |