Accepted at the Haskell Symposium’09Roll Your Own Test Bed for Embedded Real-Time Protocols:A Haskell ExperienceLee PikeGalois, [email protected] BrownIndiana [email protected] GoodloeNational Institute of AerospaceAlwyn.Goo dl [email protected] present by example a new application domain for functionallanguages: emulators for embedded real-time protocols. As a case-study, we implement a simple emulator for the Biphase Mark Pro-tocol, a physical-layer network protocol in Haskell. The surprisingresult is that a pure functional language with no built-in notion oftime is extremely well-suited for constructing such emulators. Fur-thermore, we use Haskell’s property-checker QuickCheck to au-tomatically generate real-time parameters for simulation. We alsodescribe a novel use of QuickCheck as a “probability calculator”for reliability analysis.Categories and Subject Descriptors B.8.1 [Hardware]: Perfor-mance and ReliabilityGeneral Terms Languages, Reliability, VerificationKeywords Physical-layer protocol Testing, Emulation, FunctionalProgramming1. IntroductionWe present by example a new application domain for functionallanguages: building efficient emulators for real-time systems. Real-time systems are difficult to design and validate due to the com-plex interleavings possible between executing real-time compo-nents. Emulators assist in exploring and validating a design beforecommitting to an implementation. Our goal in this report is to con-vince the reader by example1that1. one can easily roll-one’s-own test bed for embedded real-timesystems using standard functional languages, with no built-innotion of real-time;2. testing infrastructure common to functional languages, such asQuickCheck (Claessen and Hughes 2000), can be exploited togenerate real-time parameters for simulation—we generate ap-proximately 100,000 real-time parameters and execution tracesper minute on a commodity laptop;1The source code associated with this paper is presented in the Appendixand is also available for download at http://www.cs.indiana.edu/∼lepike/pubpages/qc-biphase.html. The code is released under aBSD3 license. The emulator is about 175 lines of code, and the QuickCheckinfrastructure is about 100 lines.[Copyright notice will appear here once ’preprint’ option is removed.]3. and QuickCheck can be used for a novel purpose—to do statis-tical reliability analysis.In our report, we assume that the reader is familiar with Haskellsyntax. That said, our approach uses basic concepts shared bymodern functional languages and does not intrinsically rely onlaziness (or strictness) or special monads, for example.In the remainder of this introduction, we motivate the problemdomain and describe related work before going on to describe theemulator framework.Problem Space: Physical Layer Networking The physical layerresides at the lowest level of the network stack and defines themechanism for transmitting raw bits over the network. At the phys-ical layer, bits are encoded as voltage signals. A bit stream is trans-mitted by modulating the electrical signal on an interconnect (e.g.,coaxial cable). It is not as simple as translating the 1 to high volt-age and 0 to low voltage because the receiver needs to be able todetect when there are consecutive ones or zeros and know whenthe sender has changed the signal. The inherent complexity at thislayer results from (1) the sender and receiver not sharing a hard-ware clock (so they are asynchronous) and (2) the continuity of thephysical world. Thus, the digital abstraction cannot be assumed tohold at this level. Furthermore, we must model the jitter and drift ofhardware clocks and the time an electrical signal takes to settle be-fore it stabilizes to a high or low value. If the receiver samples theinterconnect at the wrong time, the signal may be misinterpreted bythe receiver. The goal is to design a protocol and define timing con-straints to ensure the receiver samples the interconnect at the rightintervals to reliably decode the bit stream sent by the transmitter.Many physical protocols exist, but we shall focus on the BiphaseMark Protocol (BMP), which is used to transmit data in digitalaudio systems and magnetic card readers (e.g., for credit cards).The emulator is modularized: emulating another protocol requireschanging just a few small functions (about 30 lines of code).Background and Related Work Physical layer protocols havebeen a canonical challenge problem in the formal methods com-munity. Recent work uses decision procedures (more precisely,satisfiability modulo theories) and model-checking to verify theircorrectness (Brown and Pike 2006); these results compare favor-ably to previous efforts using mechanical theorem-proving, whichrequired thousands of manual proof steps (Moore 1994; Vaan-drager and de Groot 2004). Indeed, the emulator described hereis essentially refined from its high-level specification in a modelchecker (Brown and Pike 2006). Given the success of these formalverification techniques—which prove correctness—what interest isthere in simulation?There are at least a few responses. To begin with, it is not alwaysthe case that the constraints can be expressed in a decidable theory.In particular, timing constraints that contain non-linear inequalities1 2009/6/14cannot be decided (in this case, it so happens that our expressionof the BMP constraints are linear). Furthermore, decision proce-dures and model-checkers are complex and may contain bugs, orthe model itself may contain bugs. Both cases may lead to vacuousproofs, but because the “execution” of a model-checker’s model issymbolic, it can be difficult to sanity-check the correctness of themodel or tool. An emulator, however, is executed on concrete data.Another motivation is that even if there are no bugs in a formalmodel, a proof of correctness is only as good as the connection be-tween the model used in the proof and its fidelity to the implemen-tation. The components of a Haskell emulator can be, in principle,refined into digital hardware (Sheeran 2005), and the QuickCheck-generated data can be used not only to drive the emulator, but astest-vectors for the implemented hardware. Finally, as we discussin Section 5, QuickCheck can be used as a “probability calculator”for reliability analysis of digital systems, something that cannot bedone easily with current formal verification tools.The work described here is part of a larger