Citation
Arindam Chakrabarti. "A Framework for Compositional Design and Analysis of Systems". PhD thesis, UC Berkeley, December, 2007.

Abstract
Complex system design today calls for compositional design and implementation. However each component is designed with certain assumptions about the environment it is meant to operate in, and delivering certain guarantees if those assumptions are satisfied; numerous inter-component interaction errors are introduced in the manual and error-prone integration process as there is little support in design environments for machine-readably representing these assumptions and guarantees and automatically checking consistency during integration. Based on Interface Automata we propose a framework for compositional design and analysis of systems: a set of domain-specific automata-theoretic type systems for compositional system specification and analysis by behavioral specification of open systems. We focus on three different domains: component-based hardware systems communicating on bidirectional wires. concurrent distributed recursive message-passing software systems, and embedded software system components operating in resource-constrained environments. For these domains we present approaches to formally represent the assumptions and conditional guarantees between interacting open system components. Composition of such components produces new components with the appropriate assumptions and guarantees. We check satisfaction of temporal logic specifications by such components, and the substitutability of one component with another in an arbitrary context. Using this framework one can analyze large systems incrementally without needing extensive summary information to close the system at each stage. Furthermore, we focus only on the inter-component interaction behavior without dealing with the full implementation details of each component. Many of the merits of automata-theoretic model-checking are combined with the compositionality afforded by type-system based techniques. We also present an integer-based extension of the conventional boolean verification framework motivated by our interface formalism for embedded software components. Our algorithms for checking the behavioral compatibility of component interfaces are available in our tool Chic, which can be used as a plug-in for the Java IDE JBuilder and the heterogenous modeling and design environment Ptolemy II. Finally, we address the complementary problem of partitioning a large system into meaningful coherent components by analyzing the interaction patterns between its basic elements. We demonstrate the usefulness of our partitioning approach by evaluating its efficacy in improving unit-test branch coverage for a large software system implemented in C.

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-174.html

• HTML

  Arindam Chakrabarti. <a
  href="http://chess.eecs.berkeley.edu/pubs/460.html"
  ><i>A Framework for Compositional Design and
  Analysis of Systems</i></a>, PhD thesis,  UC
  Berkeley, December, 2007.

• Plain text

  Arindam Chakrabarti. "A Framework for Compositional
  Design and Analysis of Systems". PhD thesis,  UC
  Berkeley, December, 2007.

• BibTeX

  @phdthesis{Chakrabarti07_FrameworkForCompositionalDesignAnalysisOfSystems,
      author = {Arindam Chakrabarti},
      title = {A Framework for Compositional Design and Analysis
                of Systems},
      school = {UC Berkeley},
      month = {December},
      year = {2007},
      abstract = {Complex system design today calls for
                compositional design and implementation. However
                each component is designed with certain
                assumptions about the environment it is meant to
                operate in, and delivering certain guarantees if
                those assumptions are satisfied; numerous
                inter-component interaction errors are introduced
                in the manual and error-prone integration process
                as there is little support in design environments
                for machine-readably representing these
                assumptions and guarantees and automatically
                checking consistency during integration. Based on
                Interface Automata we propose a framework for
                compositional design and analysis of systems: a
                set of domain-specific automata-theoretic type
                systems for compositional system specification and
                analysis by behavioral specification of open
                systems. We focus on three different domains:
                component-based hardware systems communicating on
                bidirectional wires. concurrent distributed
                recursive message-passing software systems, and
                embedded software system components operating in
                resource-constrained environments. For these
                domains we present approaches to formally
                represent the assumptions and conditional
                guarantees between interacting open system
                components. Composition of such components
                produces new components with the appropriate
                assumptions and guarantees. We check satisfaction
                of temporal logic specifications by such
                components, and the substitutability of one
                component with another in an arbitrary context.
                Using this framework one can analyze large systems
                incrementally without needing extensive summary
                information to close the system at each stage.
                Furthermore, we focus only on the inter-component
                interaction behavior without dealing with the full
                implementation details of each component. Many of
                the merits of automata-theoretic model-checking
                are combined with the compositionality afforded by
                type-system based techniques. We also present an
                integer-based extension of the conventional
                boolean verification framework motivated by our
                interface formalism for embedded software
                components. Our algorithms for checking the
                behavioral compatibility of component interfaces
                are available in our tool Chic, which can be used
                as a plug-in for the Java IDE JBuilder and the
                heterogenous modeling and design environment
                Ptolemy II. Finally, we address the complementary
                problem of partitioning a large system into
                meaningful coherent components by analyzing the
                interaction patterns between its basic elements.
                We demonstrate the usefulness of our partitioning
                approach by evaluating its efficacy in improving
                unit-test branch coverage for a large software
                system implemented in C.},
      URL = {http://chess.eecs.berkeley.edu/pubs/460.html}
  }
  

Posted by Arindam Chakrabarti on 24 Jun 2008.
Groups: chess chesslocal
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.