Citation
Slobodan Matic. "Compositionality in Deterministic Real-Time Embedded Systems". PhD thesis, University of California, Berkeley, February, 2008.

Abstract
Many computing applications, especially those in safety critical embedded systems, require highly predictable timing properties. However, time is often not present in the prevailing computing and networking abstractions. In fact, most advances in computer architecture, software, and networking favor average-case performance over timing predictability. This thesis studies several methods for the design of concurrent and/or distributed embedded systems with precise timing guarantees. The focus is on flexible and compositional methods for programming and verification of the timing properties. The presented methods together with related formalisms cover two levels of design: - Programming language/model level. We propose the distributed variant of Giotto, a coordination programming language with an explicit temporal semantics - the logical execution time (LET) semantics. The LET of a task is an interval of time that specifies the time instants at which task inputs and outputs become available (task release and termination instants). The LET of a task is always non-zero. This allows us to communicate values across the network without changing the timing information of the task, and without introducing nondeterminism. We show how this methodology supports distributed code generation for distributed real-time systems. The method gives up some performance in favor of composability and predictability. We characterize the tradeoff by comparing the LET semantics with the semantics used in Simulink. - Abstract task graph level. We study interface-based design and verification of applications represented with task graphs. We consider task sequence graphs with general event models, and cyclic graphs with periodic event models with jitter and phase. Here an interface of a component exposes time and resource constraints of the component. Together with interfaces we formally define interface composition operations and the refinement relation. For efficient and flexible composability checking two properties are important: incremental design and independent refinement. According to the incremental design property the composition of interfaces can be performed in any order, even if interfaces for some components are not known. The refinement relation is defined such that in a design we can always substitute a refined interface for an abstract one. We show that the framework supports independent refinement, i.e., the refinement relation is preserved under composition operations.

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-12.html

• HTML

  Slobodan Matic. <a
  href="http://chess.eecs.berkeley.edu/pubs/776.html"
  ><i>Compositionality in Deterministic Real-Time
  Embedded Systems</i></a>, PhD thesis, 
  University of California, Berkeley, February, 2008.

• Plain text

  Slobodan Matic. "Compositionality in Deterministic
  Real-Time Embedded Systems". PhD thesis,  University of
  California, Berkeley, February, 2008.

• BibTeX

  @phdthesis{Matic08_CompositionalityInDeterministicRealTimeEmbeddedSystems,
      author = {Slobodan Matic},
      title = {Compositionality in Deterministic Real-Time
                Embedded Systems},
      school = {University of California, Berkeley},
      month = {February},
      year = {2008},
      abstract = {Many computing applications, especially those in
                safety critical embedded systems, require highly
                predictable timing properties. However, time is
                often not present in the prevailing computing and
                networking abstractions. In fact, most advances in
                computer architecture, software, and networking
                favor average-case performance over timing
                predictability. This thesis studies several
                methods for the design of concurrent and/or
                distributed embedded systems with precise timing
                guarantees. The focus is on flexible and
                compositional methods for programming and
                verification of the timing properties. The
                presented methods together with related formalisms
                cover two levels of design: - Programming
                language/model level. We propose the distributed
                variant of Giotto, a coordination programming
                language with an explicit temporal semantics - the
                logical execution time (LET) semantics. The LET of
                a task is an interval of time that specifies the
                time instants at which task inputs and outputs
                become available (task release and termination
                instants). The LET of a task is always non-zero.
                This allows us to communicate values across the
                network without changing the timing information of
                the task, and without introducing nondeterminism.
                We show how this methodology supports distributed
                code generation for distributed real-time systems.
                The method gives up some performance in favor of
                composability and predictability. We characterize
                the tradeoff by comparing the LET semantics with
                the semantics used in Simulink. - Abstract task
                graph level. We study interface-based design and
                verification of applications represented with task
                graphs. We consider task sequence graphs with
                general event models, and cyclic graphs with
                periodic event models with jitter and phase. Here
                an interface of a component exposes time and
                resource constraints of the component. Together
                with interfaces we formally define interface
                composition operations and the refinement
                relation. For efficient and flexible composability
                checking two properties are important: incremental
                design and independent refinement. According to
                the incremental design property the composition of
                interfaces can be performed in any order, even if
                interfaces for some components are not known. The
                refinement relation is defined such that in a
                design we can always substitute a refined
                interface for an abstract one. We show that the
                framework supports independent refinement, i.e.,
                the refinement relation is preserved under
                composition operations.},
      URL = {http://chess.eecs.berkeley.edu/pubs/776.html}
  }
  

Posted by Christopher Brooks on 13 Nov 2010.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.