Software Composition and Verification for Sensor Networks
Contents
1. 17 between the formal model and the implementation of components Model verification with existing source code especially if the code was not created with a model centric approach is a cumbersome if not impossible task Analyzing sources written in traditional procedural languages such as C implies heuristic methods Their dependency on the target implementation language makes the effort hard to justify We have chosen a different approach which interrogates the existing mod ules and instead of trying to understand the source files it generates addi tional code based on the interface models The generated software behaves like a wrapper around the component to be tested it generates each signal which is accepted by the component and it is prepared to receive all of the events coming from the module The wrapper code reckons with the specified order of events it executes the interface automata by transmitting actions in proper states and catching unexpected incoming messages Figure 9 demon strates the model verification process This simple yet powerful approach treats existing TinyOS modules as black box components therefore it can handle even the most obfuscated source code Although this approach is not adequate for exploring the entire state space of an arbitrary software compo nent we succeeded in discovering interdependencies of interface primitives in real life TinyOS components wrapper generator Componen2. The erroneous implementation of the sensor component shown in Figure 12 differs exactly in this regard The automaton depicts a typical mistake it es sentially discards an event coming from the communication component After its first iteration the sensor component may acquire a new sample from the A D module while the communication component is still in its sending state where the comm_send event is not accepted This application is unreliable its operation depends on the timing properties of the data acquisition periodic timer and task scheduling This error a reachable illegal state is caught by the automatic verification tool In contrast manual debugging of similar problems may easily become a time consuming task 8 CONCLUSIONS The presented model based approach to the component based development of sensor network applications places special emphasis on interface specifi cation The proposed formalism captures the temporal and type aspects of interfaces and supports composition and verification of components The im plementation of the prototype modeling environment and the corresponding verification tools provided valueable feedback and influenced the design of the representation methodology The sensor example clearly demonstrated the benefits of our extensions to the traditional interface automata language namely the hierachical representation 20 of states and the introduction of non preemptable conditions Compatiblity
3. pages 428 441 4 K Schneider Verification of Reactive Systems Formal Methods and Algorithms Springer Verlag 2004 5 G J Holzmann The SPIN Model Checker Primer and Reference Manual Addison Wesley 2003 6 E M Clarke Jr O Grumberg D A Peled Model Checking MIT Press 2000 7 E Mikk Y Lakhnech and M Siegel Hierarchical automata as model for statecharts Asian Computing Science Conference ASIAN 97 Vol 1345 of LNCS Springer Verlag 1997 8 N Sabadini R Walters Hierarchical Automata and P systems Electronic Notes in Theoretical Computer Science Vol 78 Elsevier 2003 9 Ji Wang Wei Dong and Zhi Chang Qi Slicing Hierarchical Automata for Model Checking UML Statecharts Proceedings of the 4th International Conference on Formal Engineering Methods Springer Verlag 2002 pages 435 446 21 10 A Speck E Pulvermiiller M Jerger B Franczyk Component Composition Validation International Journal of Applied Mathematics and Computer Science Vol 12 pages 581 589 2002 11 J Hill at al System Architecture Directions for Networked Sensors Proceedings of ASPLOS 2000 12 L deczi Bakay M Mar ti P V lgyesi G Nordstrom J Sprinkle G Karsai Composing Domain Specific Design Environments IEEE Computer 34 11 pp 44 51 November 2001 13 P V lgyesi L deczi Component Based Development of Networked Embedded Applications 28th EUROMICRO Conference EURO
4. their interface models need to handle these events in all states resulting in a potentionally large number of steps Hierarchical states enable us to simplify these often incomprehensible models getData dataRdy start stop getData dataRdy saveData Fig 4 Hierarchical interface model of Recorder Figure 4 shows the hierarchical interface model of a simple data logger com ponent Recorder By receiving a start input signal the component enters into a loop of data acquisition get Data dataRdy using for example a sensor peripheral and data storage saveData The module must be prepared to receive a stop signal and leave the loop at any moment getData dataRdy ep stop start stop getData dataRdy saveData Fig 5 Flat interface model of Recorder The flat interface model of the same component is given in Figure 5 Even for this simple component the benefits of the hierarchical model are noticeable not only because we have spared two arrows in the model but because it captures the essence of the stop signal and preserves visual clarity If the logic in the recording loop needs refinement the hierarchy ensures that the stop signal will be handled in the new states as well which is not true in the flat scenario The original Interface Automata language is a superb formalism for specifying interfaces in event driven systems where each component has its own thread of control and the components engag
5. Off redOn redOff greenOn greenOff Fig 6 Interface model of component LEDs using the original automata language The last problem has driven us to introduce another extension to the origi nal language Figure 6 depicts the interface automata of a common embed ded component that provides access to the display LEDs of the hardware Our driver is fairly simple it allows to turn off or on both of its supervised LEDs red and green Using the original interface automata language and the pessimistic compatibility rules the interface becomes incomprehensible since it needs to handle incoming requests disregarding its current state In practice this component would turn on or off all of the LEDs by using a sim ple sequence of commands in an atomic way Therefore we have introduced non preemptable states which enable us to specify atomic action sequences as shown in Figure 7 Upon entering a non preemptable state designated by solid circles multiple output actions are allowed to be sent before entering a regular state again Non preemptable states can be implemented in several ways the most trivial approach is interrupt masking or the use of mutexes The nesC language and the TinyOS concurrency model has similar constructs which make a distinction between asynchronous and synchronous code j off redOn redOff greenOn greenOff Fig 7 Interface model of component LEDs with non preemptable states The hierarchical representation o
6. attribute while the arguments are modeled with contained objects each having its own type declaration A module con tains a set of interface references interface_ref and its nesC code as a textual attribute A reference is a graphical object that points to another object con tained elsewhere in the model hierarchy This is captured in the metamodel by a directed connection pointing from the interface to the interface_ref meta model in Figure 1 Interfaces are declared at the global level and modules do not contain them directly they just refer to their declaration through the use of references This allows multiple modules using and or implementing the same interface declarations Also when an interface needs to be modified it is done at one place and all interface references in all components will refer to the updated interface automatically Similarly configurations contain references to interfaces modules module_ref and other configurations configuration_ref Interface references contained in modules and configurations appear as ports in higher level configurations Component wiring specifications are expressed in Gratis as connections be tween interfaces and or interface ports in configurations In fact two different kinds of connections are used in configurations A LINK specifies that a compo nent uses an interface that another provides An EQUATE connection specifies that the interface the given configuration uses provides is del
7. concepts to GME concepts as shown in Figure 1 The three basic building blocks of Gratis models are interfaces modules and configurations An interface consists of a _LINK_ TOSFolder _EQUATE_ lt sCannection lt Folder gt gt lt lt Connection gt gt Paaa main j DstParams field DstParams field SrcParams field t SrcParams field srclabel field p dstlabel field nesCitem dst base_interface sre lt lt Model gt gt 0 7 c sheer E InitialCode field Description field interface interface_ref L___ configuration module lt sModel gt lt lt Reference gt gt Lej lt lt Model gt lt sModel gt le InterfaceParameter enum 0 7 ModuleCode field r i y7 7 0 7 0 7 configuration_ref module_ref FunctionBase lt Reference gt gt lt Reference gt gt lt lt Model gt Argument 0 s lt Atom gt Async bool Le ____________ Description field OtherType field ReturnType enum ArgumentumType enum OtherType field event command lt lt Model gt Model gt gt Fig 1 The simplified metamodel of Gratis set events and commands Both events and commands are functions The re turn type is captured by a textual
8. that the implementation of a component matches its formal model respectively 1 INTRODUCTION Component based design is increasingly viewed as the cornerstone of software engineering The advantages of using components stem from the fact that they can be developed and tested in isolation and systems can be built and updated incrementally When they are designed with adequate generality components can be reused in different applications Component based design has become especially important for networked embedded systems where hardware plat forms and operating systems are characterized by a rapid pace of innovation Preprint submitted to Elsevier Science 27 August 2004 This is best exemplified by the advent of TinyOS 11 an operating system specifically designed for sensor networks and nesC 14 its programming lan guage Even the most basic system modules of TinyOS are components that can be augmented or replaced for different applications and or platforms The nesC language defines a component model that relies on bidirectional inter faces and admits an efficient implementation that avoids dynamic component creation TinyOS applications are statically linked graphs of event driven com ponents Typically the same application image is executed on all or most of the nodes of the network Full blown sensor network systems are built from hundreds of intricately interacting components through thousands of compo nent interfaces Manua
9. MICRO 2002 Dortmund Germany September 4 6 2002 14 D Gay P Levis R von Behren M Welsh E Brewer and D Culler The nesC Language A Holistic Approach to Networked Embedded Systems Proceedings of Programming Language Design and Implementation PLDI 2003 June 2003 15 SICStus SICStus Prolog User s Manual Swedish Institute of Computer Science Sweden 16 S J Garland and N A Lynch Using I O automata for developing distributed systems Foundations of Component Based Systems Cambridge University Press 2000 pages 285 312 17 J Warmer and A Kleppe The Object Constraint Language Getting Your Models Ready for MDA Second Edition Addison Wesley 2003 22
10. Software Composition and Verification for Sensor Networks P V lgyesi M Mar ti S D ra E Osses and A L deczi a Embedded Information Technology Research Group Hungarian Academy of Sciences Budapest University of Technology and Economics Magyar tud sok k r tja 2 Budapest 1117 Hungary gt Institute for Software Integrated Systems Vanderbilt University Nashville TN 37221 USA Abstract Component based design has become a necessity for networked embedded systems where hardware platforms come in a great variety and evolve extremely rapidly Op erating system components and higher level middleware services call for modular software construction along clear interfaces The way we describe these interfaces and process the captured information is of crucial importance to exploit the bene fits of component based design In this paper we present a model based approach to the development of embedded applications with a special emphasis on interface specification The proposed formalism captures the temporal and type aspects of interfaces and supports composition and verification of components Along with the formal definition of the proposed interface language and component compatibility rules we present a modeling environment targeting TinyOS a representative em bedded operating system Two prototype tools are also described that check the composability of components based on their interface models and verify
11. anted to create a rapid prototyping framework by reducing the time and effort needed to map formal rules into executable algorithms Note that similar motiva tions lead us to the development of the Generic Modeling Environment By analyzing the nature of our formulae we concluded that logic programming languages provide ideal ground to implement and execute these formal rules and statements Based on the visual interface specifications created in the modeling environ ment the following logical predicates are automatically generated state p s s is a state in automaton p npstate p s s is a non preemptable state in automaton p init p s s is an initial state in automaton p in p a out p a internal p a ais an input output or internal action in automaton p respectively e step p s a t there is a step in automaton p from state s to state t on action a The generated predicates capture the same information that is described in the graphical model The advantage of logic program statements is undeniable after translating our definitions to logic program rules To demonstrate the effectiveness of this approach the Prolog version of Defi nition 3 is given h The intersection of internals p and actions q is empty internal_fault P Q internal P A action Q A internal_fault P Q internal Q A action P A The intersection of outs p and outs q is empty out_fault P Q out P A out Q A The intersection o
12. are generated The built in rule for detecting invalid end states in SPIN will find all reachable illegal state configurations in the design Other interesting properties like liveliness or arbitrary assertions can also be checked by la beling certain states More sophisticated requirements can be formalized in linear time temporal logic LTL or by using never claims in the PROMELA language SPIN was created for detecting conceptual defects in distributed reactive sys tems Considering the characteristics of our domain and comparing SPIN to our original approach we should note the following difficulties e Interacting TinyOS components are not scheduled asynchronously there fore SPIN s proctype feature seems to be an overkill here e Our definition of compatiblity can easily handle open compositions i e component configurations with unbound input and output actions All un bound actions must be manually closed during model extraction since SPIN is unable to handle open systems This makes the GRATIS model translator for SPIN more complex 6 MODEL VERIFICATION Interface automata capture only the surface of software components hence these descriptions are not sufficient for automatic code synthesis or simula tion They can be constructed even after the implementation phase of the component as it is the case when dealing with existing TinyOS modules Therefore some kind of automatic verification is needed assuring consistency
13. checks with logic programs although unconventional prove to be extremely simple and straightforward to implement ensuring consistency with the formal definitions The presented extended Gratis environment significantly enhanced our TinyOS application development capabilities The nature of communication between components through function calls re quires future study since it does not fit the automata model perfectly return values and constraints inherent in sequential flow of control are not captured by the current language Our current approach of compatibility checking suffers from scalability issues the composition of n components requires O n checks among these compo nents This is not a serious limitation considering the complexity of typical TinyOS applications however it might prove to be a real problem in modeling of entire sensor networks References 1 L de Alfaro T A Henzinger Interface Automata Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering FSE ACM Press 2001 pp 109 120 2 D Harel Statecharts A Visual Formalism for Complex Systems Science of Computer Programming Elsevier Vol 8 No 3 1987 pages 231 274 3 A Chakrabarti L de Alfaro T A Henzinger M Jurdzinski and F Y C Mang Interface compatibility checking for software modules Proceedings of the 14th International Conference on Computer Aided Verification CAV LNCS Vol 2404 Springer Verlag 2002
14. e defined by a set of function declarations Compatibility checking provided by compilers guarantees that the user of a function provides the required parameters and handles the returned value in a type safe manner Even in trivial applications the access points of a software component are not isolated dependencies and complex relationships might impose additional constraints on the use of their services Typical patterns such as initialization before use can be found in almost every component A component providing communication services may have more restrictions that are inherent in the communication protocol Even if the legal order and dependencies of the func tion calls are described in the documentation of the component as informal rules automatic tools and formal methods cannot be developed to verify these constraints Graphical models of traditional interfaces enable us to understand and build complex applications however they do not extend the information captured in the textual representation Effective composition and reuse of software com ponents demands deeper understanding and specification of component inter faces Our proposed formalism based on the Interface Automata language 1 captures the dynamic aspects of component interfaces and enables us to describe more complex behavior In the following sections formal rules of interface compatibility will be given along with the description of practical methods for verif
15. e one another asynchronously via events However the concepts of interface automata cannot be mapped to typical em bedded applications easily where the software components are linked together and communicate via function calls Since our primary goal was to provide in terface models for TinyOS components we had to address the following issues e What constitutes an action in these applications Is it only the function call that conveys information or its return as well e Interface Automata make decisions based purely on the received actions unlike in procedural systems where actions are accompanied by quantitative parameters that have strong influence on the control flow e In monolithic embedded applications the assumptions of parallel execution and asynchronous message passing no longer hold Implicit constraints re strict the execution of an automaton that are inherent in sequential execu tion To address the first problem we have chosen the function calls as the sole representation of actions in the interface model Our decision was influenced by a feature provided by the nesC compiler which allows to fan out a function call to multiple components that itself raises the question of what the return value of a function means The second question may be resolved 10 by introducing multiple actions for a given function however an extension of the interface language with action parameters is an area of further study On
16. egated down to a contained component that either implements it or delegates it further down the component hierarchy GRATISII sample Sensor sample Sensor DORK jl Fie Edt View Window Hep E s PBAX NGl H sl aev lA lE Components T Name Sensor configuration Aspect Hierarchy zi Base Nja Aggregate Inheritance Meta a Sensor sample Sensor SensorM BlinkTask a Bombilla a Chin Ga CntToLeds 9 gt v x UNK Interfaces je ey ey Attributes Preferences Properties 3 9 rs pistons provides PreprocessorSet configuration_ref interface_ref module_ref FunctionBylnterface Hierarchy InterfaceAutomata Ready EDIT 100 GRATISII 11 31 AM A Fig 2 Top level model of the Sensor application in Gratis Figure 2 depicts an example application modeled in Gratis illustrating these concepts This application periodically samples a photo sensor and sends the measured readings to a base station The participating components are Main the standard entry point of all applications in TinyOS TimerC the abstrac tion layer of hardware timers Photo the photo sensor driver Comm the standard wireless communication protocol stack of TinyOS and SensorM the sole application specific module Module and configuration components are depicited in dark and light colors respectively The ports of the components are prov
17. en considered by the developer We address these sources of programming errors by introduc ing a hierarchical component verification formalism based on the Interface Automata language and by extending the Gratis environment with a proto type verification tool for TinyOS applications In the following sections we overview TinyOS and Gratis Then we formally define hierarchical interface automata our formalism for modeling component interfaces Next we define the composition and compatibility verification of hierarchical interface automata We describe how these automata can be used to validate existing hand written components as well as assemblies of compo nents Finally we illustrate the use of the proposed formalism in the extended Gratis environment 2 TINYOS TinyOS is a component based configurable operating system with a very small footprint specifically designed for severely resource constrained devices such as the nodes in a typical sensor network 11 TinyOS is a large set of software components implementing the basic functionalities that an application might need from the given device such as basic I O timers wireless communica tion etc Components can contain other components in a hierarchical fashion Each application consists of application specific components written by the application designer and a subset of the TinyOS components This way an application specific TinyOS instance is created for each application provid ing o
18. f ins p and ins q is empty in_fault P Q in P A in Q A Final rule compose_fault P Q internal_fault P Q compose_fault P Q out_fault P Q compose_fault P Q in_fault P Q After merging the translated rules and the automatically generated predicates in a Prolog 15 interpreter one can check whether two automata p and q are compatible by asking the following question compose_fault p a 16 The remaining definitions can be easily mapped as well the entire toolset for compatibility checking consists of few lines of logic program code and a trivial model translator The current implementation applies basic reachability analysis on the com posite automata by searching for illegal state configurations One of the main benefits of this approach is the extremely simple implementation of the model translator The relatively primitive structure of TinyOS interfaces allowed us to utilize this method However when more complex designs have to be veri fied or other intricate properties must be checked employing a model checker might be a more appropriate choice For these reasons we have implemented a different translator for GRATIS recently which targets SPIN 5 a well known verification tool Each automaton in GRATIS is mapped to a PROMELA proctype by trans forming automata actions to send and receive statements and state transi tions to flow control elements For each pair of components separate channels
19. f interfaces can be transformed automatically to the traditional flat notation thus the original rules of compatibility are 11 applicable to hierarchical models The introduction of non preemptable states however needs a slight modification to these formulae The formal definition of compatibility in Hierarchical Interface Automata is given in the next section The definition of hierarchical interface automata with non preemptable states follows Definition 2 A hierarchical interface automaton P consists of the following elements e Elements of regular interface automata as defined in Definition 1 e hstates P a set of hierarchical states each of which is a subset of states P and hstates P Steps originating from hstates are implicitly defined for each contained sub state Steps entering into hstates are implicitly defined for the contained initial sub state e npstates P a set of non preemptable states npstates P C states P The automaton does not accept input actions in non preemptable states Adding hierarchy to traditional finite automata is a well known and widely used extension in the domain of reactive systems The most renowned for malism is Statecharts presented by Harel 2 He introduced concurrency and communication along with hierarchy to be able to handle more com plex systems Extended Hierarchical Automata 7 which can be regarded as a kind of abstract syntax of Statecharts address similar weaknesses of trad
20. ication and validation of component interfaces and interaction We have also implemented a proof of concept prototype environment of our interface language that targets the TinyOS platform and augments the previously described Gratis tool 13 4 1 Interface Automata Our interface modeling language is based on the definition of Interface Au tomaton which we will reproduce here Definition 1 An interface automaton P consists of the following elements e states P a set of states e inits P a nonempty subset of states P known as the initial states e ins P outs P and internals P mutually disjoint sets of input output and internal actions We denote the set of all actions by acts P ins P U outs P Uinternals P and e steps P a set of steps where steps P C states P x acts P x states P A simple example of an interface automaton is given in Figure 3 The model describes the interface of the Comm component which provides communica tion services to its clients The component accepts the init and the sendM sg input actions and signals the sendDone output action However these actions are not accepted or generated arbitrarily The legal orders are defined with the help of states s0 s1 and s2 where s0 is the initial state sendMsg sendDone init sendMsg sendDone Fig 3 The Interface Automaton Comm Proper clients of this component should reckon with the temporal dependen cies between the input and o
21. ided and used interfaces This example will be used throughout the paper The only information captured textually in Gratis is the procedural code of module implementations The model translator generates all the nesC files containing interface module and configuration specifications automatically Keeping the graphical models and the corresponding nesC files in synch is a challenge especially because a large code base of TinyOS components ex ists in text form only Therefore the Gratis model translator is bi directional not only does it generate the nesC files from graphical models but it is also capable of parsing existing source files and building the corresponding mod els automatically The main use of this parsing feature is to automatically generate the graphical equivalent of the TinyOS system components and to provide them as a library to the user in the Gratis environment This library can then be refreshed when new TinyOS versions become available without any modifications to existing graphical application models 4 TEMPORAL MODELS OF COMPONENT INTERFACES Traditional programming languages and interface description methods such as CORBA IDL capture only the type aspects of software components The access points of a given component are enumerated along with their accepted and returned parameter types in terms of values and domains TinyOS and its implementation language nesC 14 is no exception to this component interfaces ar
22. itional FSMs An Extended Hierarchical Automaton is composed of a set of sequential automata whose states can be mapped to a set of au tomata which refine it A different approach results in a similar structure in 8 where Hierarchical Automata are constructed from elementary au tomata using the operations restricted product communicating parallel composition free product parallel composition with no communication and restricted sum sequential composition Components are hierarchically structured into super components in 10 where input and output behavior are separately modeled with the help of finite state machines while internal control flow is described in UML sequence charts This is in contrast to our notation where input output and internal transitions are blended in one automaton Hierarchical Interface Automata as introduced in this section also employ hierarchy to cope with complexity Non preemptable states are the other ex tension of our formalism which reflect a unique property single thread of control of our target domain Another distinct though theoretical feature is that a HIA like the original interface automaton never tries to capture the entire state space of the components Its use is restricted to describe the temporal dependencies among requests and responses The operational semantics of a HIA can be defined by a labeled transition system LTS 9 after hierarchy is eliminated with an automa
23. l wiring of components a tedious and error prone task in nesC can be automated by composition tools such as Gratis 13 However the truly challenging and especially missing ingredient for the development of mission critical large scale sensor network applications is component and composition verification Verification of embedded systems has an extensive research literature covering formal verification and model checking methods 6 Nevertheless only a se lected few approaches address the special needs of sensor networks such as the theory of Input Output Automata 16 and that of Interface Automata 1 The automata theoretic approach lends itself naturally to the study of networked sensor applications because of their inherent event driven nature Existing methodologies do not exploit the massively componentized and hierarchical structure of nesC programs In such designs the reactions between moderately sized software components are restricted by the single flow of control within the application as opposed to a distributed system with asynchronously scheduled processes 4 This work is focused on the modeling and light weight verifica tion of such component systems and does not claim unrestricted applicability in other domains Most programming errors during application composition are either the result of incorrectly used components or the bad interaction of multiple components some of which could be operating system components not ev
24. lity The pessimistic approach defines two compo nents incompatible if any illegal state is reachable in their composition i e there exists a sequence of steps whose first state is one of the initial compos ite states and whose last state is the illegal state The optimistic approach considers two components compatible if there is some environment a third automaton under which the composite automaton behaves correctly The pessimistic approach demands strict compatibility and it guarantees that independently of additional components the inspected modules will work together correctly When the product system is closed i e each action is internal the pessimistic and optimistic approaches coincide 1 In this paper we are following the pessimistic approach a detailed discussion of the opti mistic method can be found in 3 4 2 Hierarchical Interface Automata Interface Automata have similar limitations to Finite State Machines in their flat form both languages have scalability problems when describing complex behavior and state space We propose additional constructs to the original automata language to overcome these problems In embedded applications external events from the physical environment might arrive in any moment regardless of the current state of the application These external events are propagated through the software components via interrupts and function calls Therefore to build compatible components
25. lly analyzable and optimiz able The three major building blocks of a nesC application are interfaces modules and configurations An interface is a set of related events and or commands In other words an interface is a set of function declarations The provider of an interface needs to implement the commands while the user of the interface needs to implement the events Modules and configurations are both components Modules are the elementary building blocks they have actual procedural nesC code associated with them specifying their functionality Configurations are the composite components they contain modules and or other configurations and the wiring specification connecting the various interfaces of the contained components together Every nesC and TinyOS application has a single top level configuration 14 3 GRATIS A TinyOS application is a hierarchical component assembly where component configurations i e wiring specifications interface declarations and module im plementations are specified in numerous text files Graphical representation of the same information increases the readability and understandability of the application architecture and helps in avoiding configuration errors such as the omission of the wiring specification of one or more interfaces of a component The Graphical Development Environment for TinyOS Gratis is a typical ap plication of Model Integrated Computing MIC in general and the Generic M
26. meter enum IsPreemptable bool 0 IsFinal bool 0 _STEP_START_ lt lt Connection gt ra mState lt lt Model gt gt ft Action dst lt lt FCO gt gt ste oF FCO os _STEP_END_ Jan nen dence OT sede Connection gt gt iState lt lt Model gt gt FunctionBase lt lt Atom gt gt actionRef lt lt Reference gt gt Description field OtherType field ReturnType enum Async bool event lt lt Atom gt gt Fig 8 The metamodel of the Hierarchical Interface Automata language command lt lt Atom gt gt 13 4 4 Composition Rules We consider two hierarchical interface automata composable if there is no conflict between their actions thus they only possess common actions which move the product automaton along shared steps Definition 3 Two interface automata P and Q are composable if states P N states Q 3 internals P N acts Q internals Q N acts F outs P N outs Q 0 0 ins P Nins Q Considering Definition 3 one might notice that we made a very important assumption on the state space of the primary automata Our rules for compo sition prohibit state interference i e composition of components with shared variables or channels Although states are defined as abstract artifacts in Def inition 2 this assumption is inherent and justified i
27. n the domain of TinyOS applications where shared data areas among components are not allowed 11 This limitation enforced by the nesC compiler 14 is a trade off for sup porting isolated development and testing of TinyOS components As we have seen previously the composite automaton consists of the product of the original leaf states and the conjunction of actions reduced by the set of joint actions Composite steps are defined as for normal interface automata the only difference is in the special treatment of intermediate states input actions in the original automata are not accepted while the other component resides in a non preemptable state Definition 4 If two interface automata P and Q are composable their prod uct P x Q is defined by states P x Q states P x states Q npstates P x Q s t states P x Q s npstates P V t npstates Q inits P x Q inits P x inits Q ins P x Q ins P Uins Q S outs P x Q outs P Uouts Q S internals P x Q internals P U internals Q U S 14 steps P x Q s a s s a s steps P a SAt states Q npstates Q v t a t steps Q a S s states P npstates P V s 4 5 steps P A t a t steps Q Aa s i where S acts P N acts Q Based on the informal description of illegal states in 4 1 their precise defini tion is the key step towards understanding compatibilit
28. nly the services the application needs which conserves precious system resources A TinyOS application consisting of a set of interconnected components is scheduled by a simple FIFO based non preemtive scheduler Components com municate with each other through commands and events Commands prop agate downward they are issued by higher level components to lower level ones Events propagate upward they are signaled by lower level components and handled by higher level ones Events at the lowest level are generated by the hardware itself in the form of interrupts Commands are typically handled by updating the state of component possi bly posting a task for later execution and possibly issuing commands to lower level components An event handler can also modify the state of the com ponent signal higher level events or call lower level commands Notice that commands cannot signal events to avoid cycles Tasks are the worker bees of TinyOS They can issue commands signal events and post other tasks Tasks are intended to do a short amount of processing and return They can only be preempted by events not by other tasks This task model enables TinyOS to have a single call stack The latest version of TinyOS version 1 1 is implemented in nesC 14 nesC an extension of C is a new language developed specifically to support the TinyOS model of computation It disallows dynamic memory allocation and dynamic dispatch making nesC programs statica
29. odeling Environment GME in particular 12 GME is a metaprogramma ble toolkit for creating domain specific modeling environments GME meta models specify the modeling language of the application domain They are used to automatically configure GME for the domain that is to create a modeling environment that has native support of the target modeling lan guage GME models take the form of graphical multi aspect attributed entity re lationship diagrams Their syntax is defined by the metamodels specified in a UML class diagram based notation The static semantics of a model are specified by OCL constraints 17 that are also part of the metamodels They are enforced by a built in constraint manager during model building time The dynamic semantics are applied by the model translators i e by the process of translating the models to source code configuration files database schema or any other artifact the given application domain calls for This approach fits component based software development very nicely The interface of the individual components can be modeled along with a link to their implementation The model editor can enforce the composition rules to make sure that only valid component assemblies are allowed More sophisti cated analysis can be performed by interfacing to outside tools Finally model translators can generate the glue code that ties the final system together The metamodel of Gratis defines the mapping of TinyOS
30. t Tester model by Fig 9 The model verification process The prototype implementation of our black box testing approach targets the TinyOS platform It requires manual intervention in those interface states where alternative output steps can be made by the tester though automatic exhaustive testing could be easily achieved as well This tool has been inte grated into the Gratis environment 7 CASE STUDY To demonstrate the expressiveness of the hierarchical interface automata lan guage and the benefits of automatic composition checks we further refine the visual model of the Sensor application introduced in Figure 2 In addition 18 std_start adc_start comm_start timer_start teses C std_init l l Nera are ree comm_stop adc_stop timer_stop std_stop eee eee Fig 10 Top level model of the Sensor component Non preemptable states are used extensively timer_fired watingfordata 7 timer_fired adc_getData T adc_dataReady comm_sendDone A k d comm_send a timer_fired Fig 11 Model of the Sensor component s busy loop to presenting compatible temporal models of the central and communication components an alternative implementation will be shown where a small design flaw renders the application unreliable The top level model of the Sensor component is given in Figure 10 The lengthy action seq
31. tic transforma 12 tion The transformation builds a flat model by collecting all leaf states and inserting additional transitions based on Definition 2 4 8 Visual Language Specification Temporal interface models complement the traditional interfaces of TinyOS components thus integrating these automaton concepts into the existing Gra tis language is the natural choice The metamodel of the hierarchical interface automata language is shown in Figure 8 The module interface and Function Base meta objects are joint concepts in the original Gratis and the automata language they connect the type based and temporal models The multi aspect capability 12 of the modeling environment enables the separate visualization of the alternative representations of component interfaces The apparent sym metry in the metamodel stems from the fact that the language can capture the temporal models of both components and interfaces TinyOS interfaces and modules can contain states mState and iState that can be nested and actions actionRef and FunctionBase that can be used to connect states Special boolean attributes of the state object may designate it as an initial s nit or non preemptable sPreemptable state HasTransition lt lt Model gt gt module State interface lt lt Model gt gt lt lt Model gt gt lt lt Model gt fa n ModuleCode field Isinit bool 0 7 InterfacePara
32. uences perform initalization startup and stop procedures Upon receiving initialization startup stop requests the sensor component ini tializes starts stops the lower components subsequently Note how non pre emptive states denoted by filled circles prevent the model from growing com plicated and unreadable The started state is refined in Figure 11 Without the use of hierarchical modeling the std_stop action would have to be handled separately in each sub state of started In the started state the automaton re peatedly waits for timer events requests data from the A D converter sends samples through the communication channel and then waits for the message buffer to be cleared The temporal model of the corresponding communication component is shown in Figure 13 Albeit only the inner service loop is shown the model presents the restriction of the communication stack clearly it is not prepared to process multiple messages simultaneously 19 comm_sendDone timer_fired TS O ratnarorata 7 timer_fired adc_getData 0 o comm_send adc_dataReady Fig 12 Model of the faulty Sensor component s busy loop send i lt sendDone Fig 13 Model of the Comm component s service loop The sensor component overcomes this limitation by waiting for a sendDone event before completing the iteration thereby facilitating trivial flow control in the system
33. utput actions of Comm For instance they must not send a second consecutive send Msg action to Comm without waiting for a sendDone message before Detailed informal description of compatibility of components is given in Section 4 1 along with the exact definition in Def 6 A trivial compatible component App can be constructed by replicating the states and steps of component Comm but inverting the direction of its ac tions thus input actions in Comm become output actions in App and vice versa In their composition the two automata are advancing together step by step always transmitting or receiving an action that is accepted or sent by the other Formal definition of composite automata will be given in 4 4 In general the cross product of the set of states in the original components generates the state space of the composite automaton A step in the product might be either a shared step which advances both of the original automata together as we have seen in the previous paragraph or an independent step in one of the components Actions along shared steps become internal actions in the product automaton Compatibility analysis must focus on composite states where one of the origi nal automata initiates a shared step but the other component is not prepared for accepting this action in its respective state We denote these composite states as illegal states There are two basic approaches to classify illegal states with respect to compatibi
34. y between components Compared to the informal description of illegal states given earlier we had to alter the definition because non preemptable states are excluded from the analysis Definition 5 The set of illegal states in the product of hierarchical interface automata P and Q is defined by illegals P x Q s t s t states P x Q A Ja E S outs P At npstates Q A A s a s steps P A A t a t steps Q v a E outs Q A s npstates P A A t a t steps Q A s a 8 steps P Y According to the pessimistic approach one has to traverse the composite inter face automaton from its initial state to decide on compatibility between the components Definition 6 We consider two hierarchical interface automata P and Q compatible if no illegal states in the product automata can be reached from the initial states 5 COMPATIBILITY CHECKING Based on the previous definitions several algorithms can be developed using graph or game theoretical 1 foundations Collecting reachable states and analyzing each of them suggests graph traversing logic while the interaction of two interface automata might be easily solved by a game between the com ponents 15 Similarly to the extended interface language the rules of compatibility have been evolved gradually thus implementing an re implementing custom algo rithms for these changing ruleset would have burdened our work We w
Download Pdf Manuals
Related Search