Citation
Arkadeb Ghosal. "A Hierarchical Coordination Language for Reliable Real-Time Tasks". PhD thesis, EECS Department, University of California, Berkeley, January, 2008.

Abstract
Complex requirements, time-to-market pressure and regulatory constraints have made the designing of embedded systems extremely challenging. This is evident by the increase in effort and expenditure for design of safety-driven real-time control dominated applications like automotive and avionic controllers. Design processes are often challenged by lack of proper programming tools for specifying and verifying critical requirements (e.g. timing and reliability) of such applications. Platform based design, an approach for designing embedded systems, addresses the above concerns by separating requirement from architecture. The requirement specifies the intended behavior of an application while the architecture specifies the guarantees (e.g. execution speed, failure rate etc). An implementation, a mapping of the requirement on the architecture, is then analyzed for correctness. The orthogonalization of concerns makes the specification and analyses simpler. An effective use of such design methodology has been proposed in Logical Execution Time (LET) model of real-time tasks. The model separates the timing requirements (specified by release and termination instances of a task) from the architecture guarantees (specified by worst-case execution time of the task). This dissertation proposes a coordination language, Hierarchical Timing Language (HTL), that captures the timing and reliability requirements of real-time applications. An implementation of the program on an architecture is then analyzed to check whether desired timing and reliability requirements are met or not. The core framework extends the LET model by accounting for reliability and refinement. The reliability model separates the reliability requirements of tasks from the reliability guarantees of the architecture. The requirement expresses the desired long-term reliability while the architecture provides a short-term reliability guarantee (e.g. failure rate for each iteration). The analysis checks if the short-term guarantee ensures the desired long-term reliability. The refinement model allows replacing a task by another task during program execution. Refinement preserves schedulability and reliability, i.e., if a refined task is schedulable and reliable for an implementation, then the refining task is also schedulable and reliable for the implementation. Refinement helps in concise specification without overloading analysis. The work presents the formal model, the analyses (both with and without refinement), and a compiler for HTL programs. The compiler checks composition and refinement constraints, performs schedulability and reliability analyses, and generates code for implementation of an HTL program on a virtual machine. Three real-time controllers, one each from automatic control, automotive control and avionic control, are used to illustrate the steps in modeling and analyzing HTL programs. Advisor: Alberto L. Sangiovanni-Vincentelli and Thomas A. Henzinger

Electronic downloads

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

• HTML

  Arkadeb Ghosal. <a
  href="http://chess.eecs.berkeley.edu/pubs/463.html"
  ><i>A Hierarchical Coordination Language for
  Reliable Real-Time Tasks</i></a>, PhD thesis, 
  EECS Department, University of California, Berkeley,
  January, 2008.

• Plain text

  Arkadeb Ghosal. "A Hierarchical Coordination Language
  for Reliable Real-Time Tasks". PhD thesis,  EECS
  Department, University of California, Berkeley, January,
  2008.

• BibTeX

  @phdthesis{Ghosal08_HierarchicalCoordinationLanguageForReliableRealTime,
      author = {Arkadeb Ghosal},
      title = {A Hierarchical Coordination Language for Reliable
                Real-Time Tasks},
      school = {EECS Department, University of California, Berkeley},
      month = {January},
      year = {2008},
      abstract = {Complex requirements, time-to-market pressure and
                regulatory constraints have made the designing of
                embedded systems extremely challenging. This is
                evident by the increase in effort and expenditure
                for design of safety-driven real-time control
                dominated applications like automotive and avionic
                controllers. Design processes are often challenged
                by lack of proper programming tools for specifying
                and verifying critical requirements (e.g. timing
                and reliability) of such applications. Platform
                based design, an approach for designing embedded
                systems, addresses the above concerns by
                separating requirement from architecture. The
                requirement specifies the intended behavior of an
                application while the architecture specifies the
                guarantees (e.g. execution speed, failure rate
                etc). An implementation, a mapping of the
                requirement on the architecture, is then analyzed
                for correctness. The orthogonalization of concerns
                makes the specification and analyses simpler. An
                effective use of such design methodology has been
                proposed in Logical Execution Time (LET) model of
                real-time tasks. The model separates the timing
                requirements (specified by release and termination
                instances of a task) from the architecture
                guarantees (specified by worst-case execution time
                of the task). This dissertation proposes a
                coordination language, Hierarchical Timing
                Language (HTL), that captures the timing and
                reliability requirements of real-time
                applications. An implementation of the program on
                an architecture is then analyzed to check whether
                desired timing and reliability requirements are
                met or not. The core framework extends the LET
                model by accounting for reliability and
                refinement. The reliability model separates the
                reliability requirements of tasks from the
                reliability guarantees of the architecture. The
                requirement expresses the desired long-term
                reliability while the architecture provides a
                short-term reliability guarantee (e.g. failure
                rate for each iteration). The analysis checks if
                the short-term guarantee ensures the desired
                long-term reliability. The refinement model allows
                replacing a task by another task during program
                execution. Refinement preserves schedulability and
                reliability, i.e., if a refined task is
                schedulable and reliable for an implementation,
                then the refining task is also schedulable and
                reliable for the implementation. Refinement helps
                in concise specification without overloading
                analysis. The work presents the formal model, the
                analyses (both with and without refinement), and a
                compiler for HTL programs. The compiler checks
                composition and refinement constraints, performs
                schedulability and reliability analyses, and
                generates code for implementation of an HTL
                program on a virtual machine. Three real-time
                controllers, one each from automatic control,
                automotive control and avionic control, are used
                to illustrate the steps in modeling and analyzing
                HTL programs. Advisor: Alberto L.
                Sangiovanni-Vincentelli and Thomas A. Henzinger},
      URL = {http://chess.eecs.berkeley.edu/pubs/463.html}
  }
  

Posted by Christopher Brooks on 24 Jun 2008.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.