This directory contains an ACSR implementation of the Philips Audio Control Protocol. (Described in D. Bosscher, I. Polak, and F. Vaandrager, "Verification of an Audio Control Protocol." In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, FTRTFT '94: Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in Computer Science 863, pages 170-192. Springer-Verlag, 1994. A copy of this paper is in ./philips.ps.) The protocol describes independent sender and receiver processes that use Manchester encoding to transmit an arbitrary stream of bits over a bus. Due to hardware limitations the receiver can only detect rising edges in the signal. Zero bits (represented in Manchester encoding as falling edges) have to be inferred from timing parameters and the absence of rising edges. The sender and receiver processes have independent clocks that may drift from a hypothetical global time standard by a factor of T (i.e. if the "real" time is X, then the sender's notion of the time will be anywhere in the range [X-X*T,X+X*T]; likewise for the receiver). In the Philips protocol T is limited to 1/20 or less. The Bosscher et. al paper presents a formal model of the protocol using "linear hybrid systems" (an extension of Lynch and Vaandrager's timed I/O automata) and manual analysis proving that the protocol is correct for arbitrary inputs iff T < 1/17. The Cornell HyTech system has been used to model the protocol and automatically demonstrate correctness for inputs of eight bits or less at specific values of T. Both of these analyses were done in a dense time domain. ./philips.acsr contains an ACSR implementation of the protocol and a test process that generates bit streams and checks the outputs produced by the implementation. VERSA produces the following results: Q T | Deadlocks? states edges CPU time (secs) --- ------ + ---------- ------ ------ --------------- 1. 10 1/20 | No 7172 10301 11.21 2. 20 1/20 | No 26146 38698 52.36 3. 30 1/20 | No 56668 84843 148.82 4. 40 1/20 | No 99234 149400 323.53 5. 38 1/19 | No 94914 143656 315.64 6. 36 1/18 | No 90594 137912 276.78 7. 34 1/17 | Yes 86300 132202 273.14 8. 32 1/16 | Yes 82056 126616 239.93 9. 30 1/15 | Yes 77788 121056 226.76 Parameter Q is the duration of a quarter of a clock cycle. Parameter T is the maximum clock drift factor (as above). A deadlock indicates failure of the protocol to encode/decode data correctly. States/edges is the size of the un-minimized LTS constructed by VERSA. CPU time is for LTS construction on a SPARCstation 5 with 56 MB of memory. VERSA was compiled at -O0 (no optimization) with some debugging code enabled. The CPU times could probably be reduced if optimization was enabled and the debugging code was disabled. In the Philips protocol Q is 222 microseconds. The current LTS construction routines in VERSA can't cope with delays of that magnitude so Q had to be scaled back to 40 or less. In cases 4-9 the value of Q was selected so that the resulting LTS was manageable and Q*T was an integer. The ACSR implementation uses time extensively, priority occasionally (to insure nondeterministic choices for clock drift and two nondeterministic conditions that are described by the protocol), and resources never. Duncan dclarke@saul.cis.upenn.edu