Software composition and verification for sensor networksIntroductionTinyOSGratisTemporal models of component interfacesInterface automataHierarchical interface automataVisual language specificationComposition rulesCompatibility checkingModel verificationCase studyConclusionsReferencesScience of Computer Programming 56 (2005) 191–210www.elsevier.com/locate/scicoSoftware composition and verification forsensor networksP. Völgyesia,M.Marótib,∗,S.Dórab,E.Ossesb,Á.LédeczibaEmbedded Information Technology Research Group, Hungarian Academy of Sciences – Budapest University ofTechnology and Economics, Magyar tudósok körútja 2, Budapest, 1117, HungarybInstitute for Software Integrated Systems, Vanderbilt University, Nashville, TN 37221, USAReceived 6 November 2003; received in revised form 2 September 2004; accepted 6 September 2004Available online 13 December 2004AbstractComponent-based design has become a necessity for networked embedded systems wherehardware platforms come in a great variety and evolve extremely rapidly. Operating systemcomponents and higher level middleware services call for modular software construction alongclear interfaces. The way we describe these interfaces and process the captured information is ofcrucial importance for exploitingthe benefits of component-based design. In this paper we presentamodel based approach to the development of embedded applications with a special emphasis oninterface specification. The proposed formalism captures the temporal and type aspects of interfacesand supports the composition and verification of components. Along with the formal definitionof the proposed interface language and component compatibility rules, we present a modelingenvironment targeting TinyOS, a representative embedded operating system. Two prototype toolsare also described that check thecomposability of components based on theirinterface models andverify that the implementation of a component matches its formal model, respectively.© 2004 Elsevier B.V. All rights reserved.1. IntroductionComponent-based design is increasingly viewed as the cornerstone of software en-gineering. The advantages of using components stem from the fact that they can be∗Corresponding author.E-mail address: [email protected] (M. Maróti).0167-6423/$ - see front matter © 2004 Elsevier B.V. All rights reserved.doi:10.1016/j.scico.2004.11.012192 P. Völgyesi et al. / Science of Computer Programming 56 (2005) 191–210developed and tested in isolation, and systems can be built and updated incrementally.When they are designed with adequate generality, components can be reused in differentapplications. Component-based design has become especially important for networkedembedded systems where hardware platforms and operating systems are characterizedby a rapid pace of innovation. This is best exemplified by the advent of TinyOS[7], an operating system specifically designed for sensor networks, and nesC [5], itsprogramming language. Even the most basic system modules of TinyOS are componentsthat can be augmented or replaced for different applications and/or platforms. The nesClanguage defines a component model that reliesonbidirectional interfaces and admits anefficient implementation that avoids dynamic component creation. TinyOS applicationsare statically linked graphs of event-driven components. Typically, the same applicationimage is executed on all (or most of) the nodes of the network. Full-blown sensor networksystems are built from hundreds of intricately interacting components through thousandsof component interfaces. Manual wiring of components, a tedious and error prone taskin nesC, can be automated by composition tools, such as Gratis [15]. However, the trulychallengingand especially missing ingredientfor the development of mission critical, largescale sensor network applications is component and composition verification.Verification of embedded systems has an extensive research literature covering formalverification and model checking methods [2]. Nevertheless, only a selected few approachesaddress the special needs of sensor networks, such as the theory of Input Output Automata[4]andthatof Interface Automata [3]. The automata-theoretic approach lends itselfnaturally to the study of networked sensor applications, because of their inherent event-driven nature. Existing methodologies do not exploit the massively componentized andhierarchical structure of nesC programs. In such designs the reactions between moderatelysized software componentsarerestricted bythe single flow ofcontrol within the applicationas opposed to a distributed system with asynchronously scheduled processes [12]. Thiswork is focused on the modeling and light weight verification of such component systemsand does not claim unrestricted applicability in other domains.Most programming errors during application composition are either the result ofincorrectly used components or the bad interaction of multiple components, some ofwhichcould be operating system components not even considered by the developer. Weaddress these sources of programming errors by introducing a hierarchical componentverification formalism based on the Interface Automata language and by extending theGratis environment with a prototype verification tool for TinyOS applications.In the following sections we overview TinyOS and Gratis. Then we formally definehierarchical interface automata, our formalism for modeling component interfaces. Nextwe define the composition and compatibility verification of hierarchical interfaceautomata.We describe how these automata can be used to validate existing hand-written components,as well as assemblies of components. Finally, we illustrate the use of the proposedformalism in the extended Gratis environment.2. TinyOSTinyOS is acomponent-basedconfigurableoperating system with a very small footprintspecifically designed for severely resource constrained devices such as the nodes in aP. Völgyesi et al. / Science of Computer Programming 56 (2005) 191–210 193typical sensor network [7]. TinyOS is a large set of software components implementingthe basic functionalities that an application might need from the given device, such asbasic I/O, timers, wireless communication,etc. Components can contain other componentsin ahierarchical fashion. Each application consists of application-specific componentswritten by the application designer and a subset of the TinyOS components. This wayan