This paper, as the name suggests, formalizes certain elements of TinyOS, an operating system that has become popular in the domain of sensor networks. The well-known formalism of communicating sequential processes (CSP) is used for modeling TinyOS, as there is a good match between the elements of CSP and TinyOS, such as concurrency and event-driven computation. The formalization involves translating programs written in nesC, the application language used in TinyOS, into CSP. This translation captures the interactions between multiple TinyOS applications. Besides this, CSP models of the scheduling, preemption, and priority mechanisms of TinyOS are also developed. The formalization is illustrated with a simple example of a TinyOS application.

The motivation for the work is that a formal model of an application can be subjected to rigorous analysis, which can reveal subtle concurrency-related errors that are common in such applications.

This well-written paper is easy to read and understand. That being said, I would have liked more illustrations and examples from real applications that bring out the need for formalization. The paper would be useful to beginners who are interested in formalizing concurrent systems, and for application developers wanting a better understanding of the TinyOS model.