Testing Real-Time Properties of Embedded Systems

The authors introduce an executable model for verifying real-time properties of embedded systems programmed under PicOS, which is a tiny operating system for small-footprint wireless devices. One of its interesting features is a close relationship with a simulation/specification package, dubbed SMURPH/SIDE, offering a frugal, powerful, and friendly programming paradigm for multithreaded reactive applications. By inheriting that paradigm, PicOS threads become amenable to simulation and emulation techniques that facilitate testing and rapid prototyping of embedded systems. In this paper, they show how those techniques can be harnessed to diagnosing problems with real-time behavior of embedded applications.