Using Interface Theories for Component based Design Arindam Chakrabarti Mentors Marcin Jurdzinski Freddy Y C Mang Thomas A Henzinger Luca de Alfaro Acknowledgements Marcin Jurdzinski Freddy Y C Mang Thomas A Henzinger Luca de Alfaro Christoph Meyer Kirsch Outline of the talk Introduction Motivation Related work Some simple IA formalisms for software algorithms TinyOS example IA formalism algorithm bugs Implementation Issues Introduction Interfaces vs Components Input universal vs Input existential Friendly environment Composition Compatibility Refinement See Interface Automata by de Alfaro H Motivation Type Systems for Component Interaction Design documentation Low cost verification Design time debugging Correctness by construction See Interface Theories for Component based Design by de Alfaro H Related Work Bandera Slicing Abstract interpretation Design by Contract Jass JMSAssert JContractor iContract HandShake Java with assertions Eiffel Code instrumentation run time checks CANVAS Static heap analysis Behavioral Types Dependent Types Object Calculi Some simple IA formalisms applied to software systems Stateless I O Interfaces applied to software systems Output ports OF Method call sites Available ports IF Public abstract methods Input ports IF IF Public methods implemented Composition Analogous to Stateless I O Interfaces Connection Two channels cannot have the same source Hierarchy Must accept all inputs may not produce all outputs Stateless I O Interfaces for TinyOS Init txbev pwr rxm txm txb rxbev RFM int Init txbytes pwr txdone txbrdy rxbrdy Radio Byte Init pwr txbev rxm txm txb rxbev IA given can be checked with IA automatically extracted from code Interesting properties can be checked 1 Access Control violations 2 Namespace clashes 3 Module dependencies Stateless P D Interfaces applied to software systems Stateless 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 code Examples 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 necessary Number of paths exponential in size of graph Length of longest path NP Complete Is that a problem Stateful A G Interfaces applied to software systems Set of variables Set of valuations Set of local methods For each local method a precondition set of valuations Operators N D choice Guarded choice on valuations Valuation assignment local external method call A program graph with nodes corresponding to valuation assignments and local external method calls Edges corresponding to N D or valuation guarded choices and valuation assignments Each node in a program a program counter value For each method a program The Game Ability of the environment to prevent a local method being called when its precondition is not true Push down semantics Compatibility Check Algorithm For each local method evaluate the set of valuations where it can be invoked by bottom up recursive game evaluation For operator Valuation assignment N D choice Choice on valuations Local method call External method call U S1 T A U S1 X t S2 S1 t T A U A T1 Tk U Tk A U S1 A Sk T1 Tk U s S i 1 2 k s Si s Ti A U e A C1 Cl T1 Tl U0 T Ui 1 T Ti U i TinyOS Bugs Init Pwron init Radio Byte rxmod e Li Implementation Issues UI Interface Parser Internal Representati on IA Comp Algo BDD Package Current Status of Implementation Generic UI Interface module for plugging into JBuilder ready Parser module SableCC Any EBNF grammar spec can be plugged in for your favourite IA specification language Internal Representation module Can be plugged in with your favourite IA Compatibility Check Module Compatibility Check Algorithms Asynchronous IA done No 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 implemented Some 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 al Thanks for your time
View Full Document
Unlocking...