PowerPoint PresentationSlide 2Slide 3Slide 4Slide 5Slide 6Slide 7Slide 8Slide 9Slide 10Slide 11Slide 12Slide 13Slide 14Slide 15Slide 16Slide 17Slide 18Slide 19Slide 20Slide 21Slide 22Slide 23Slide 24Slide 25Using Interface Theories for Component based DesignArindam ChakrabartiMentors:Marcin JurdzinskiFreddy Y C MangThomas A HenzingerLuca de AlfaroAcknowledgementsMarcin JurdzinskiFreddy Y C MangThomas A HenzingerLuca de AlfaroChristoph Meyer KirschOutline of the talk• Introduction + Motivation• Related work• Some simple IA formalisms for software + algorithms• TinyOS example + IA formalism + algorithm + bugs• Implementation IssuesIntroduction• Interfaces vs Components• Input universal vs Input existential• Friendly environment• Composition • Compatibility• RefinementSee “Interface Automata” by de Alfaro/HMotivation• Type Systems for Component Interaction• Design & documentation• Low cost verification• Design time debugging• Correctness by constructionSee “Interface Theories for Component-based Design” by de Alfaro/HRelated Work• BanderaSlicing, Abstract interpretation• Design by Contract - Jass, JMSAssert, JContractor, iContract, HandShake, Java with assertions, EiffelCode instrumentation, run time checks• CANVAS Static heap analysis• Behavioral Types, Dependent Types, Object CalculiSome simple IA formalisms applied to software systems• Stateless I/O Interfaces applied to software systemsOutput ports OF : Method call sitesAvailable ports IF+ : Public abstract methodsInput ports IF IF+ : Public methods implementedComposition: Analogous to Stateless I/O InterfacesConnection: Two channels cannot have the same sourceHierarchy: Must accept all inputs, may not produce all outputsStateless I/O Interfaces for TinyOSintRFM Init pwr rxm txm txb rxbev txbevInit pwr rxm txm txb rxbev txbevRadio Byte Init txbytes pwr txbrdy rxbrdy txdone• IA given can be checked with IA automatically extracted from code• Interesting properties can be checked1. Access Control violations2. Namespace clashes3. Module dependencies• Stateless P/D Interfaces applied to software systemsStateless I/O interface• Dependency relation IF X IF OF(x,y) in implementation of local method x invokes local or output method y• Compatibility definition can be generalised based on requirements• IA can still be automatically generated from codeExamples of compatibility criteria for P/D• No recursion: No cycle in transitive closure of : Necessary and sufficient• Maximum nesting of function calls k: Maximum length of any path k in transitive closure of Sufficient but not necessaryNumber of paths exponential in size of graphLength of longest path: NP-CompleteIs that a problem ?• Stateful A/G Interfaces applied to software systemsSet of variablesSet of valuationsSet of local methodsFor each local method, a precondition (set of valuations)Operators: N/D choice, Guarded choice (on valuations),Valuation assignment, local/external method callA program: graph with nodes corresponding to valuation assignments and local/external method calls;Edges corresponding to N/D or valuation guarded choices and valuation assignmentsEach node in a program: a program counter valueFor each method, a programThe Game: Ability of the environment to prevent a local method being called when its precondition is not truePush down semanticsCompatibility Check Algorithm• For each local method, evaluate the set of valuations where it can be invoked by bottom up, recursive game evaluationFor operator• Valuation assignment• N/D choice• Choice on valuations• Local method call• External method callS1UATU = S1 X { t S2 : (S1,t) T} AUA…T1TkU = Tk AUA…T1TkS1SkU = { s S: i = 1,2,…k.s Si s Ti} AUA…T1TlC1CleU0 = T Ui+1 = T Ti UiTinyOS BugsinitInit:Radio ByterxmodePwron: LiImplementation IssuesIA Comp AlgoUI InterfaceParserBDD PackageInternal RepresentationCurrent Status of ImplementationGeneric UI Interface module for plugging into JBuilder: readyParser module: SableCC. Any EBNF grammar spec can be plugged in for your favourite IA specification languageInternal Representation module: Can be plugged in with your favourite IA Compatibility Check ModuleCompatibility Check Algorithms:• Asynchronous IA: doneNo games. Silent environment is friendly•Synchronous Stateful A/G IA: done (inefficient, with explicit state enumeration in specifications, no predicates, BDDS not used)• Synchronous Stateful A/G IA with predicates and using BDDS: being implemented• Symbolic Compatibility Check Algo for Stateful IA with pushdown semantics: being implementedSome References•Interface Automata, Luca de Alfaro, Thomas A Henzinger, FSE 2001•Interface Theories for Component based Design, Luca de Alfaro, Thomas A Henzinger, EMSOFT 2001•jContractor: A Reflective Java Library to Support Design by Contract•System Architecture Directions for Networked Sensors, Kris Pister et al•Bandera: Extracting Finite-state Models from Java Source Code, John Hatcliff et al•Behavioral Contracts and Behavioral Subtyping, Findler et al•SableCC, an Object-Oriented Compiler Framework, Gagnon et alThanks for your time
View Full Document
Unlocking...