Abstract
RAFAEL is a tool designed to assist analysis of programs written in the real-time system specification language L. The aim of such analysis is to establish properties associated with communication and synchronization between processes. First, a program in L is translated into a fifo Petri net. A fifo Petri net is an extension of a Petri net, which is particularly suitable for modelling nets of processes communicating by way of messages, which is a feature of L. The translator sifts out the communication aspect. Analysis can be conducted using one of the two algorithms: the first provides an invariant generator, the second constructs the reachability graph.
| Original language | English |
|---|---|
| Title of host publication | Unknown Host Publication Title |
| Publisher | Engl |
| Pages | 1-7 |
| Number of pages | 7 |
| ISBN (Print) | 0946536015 |
| Publication status | Published - 1 Dec 1984 |