Citation
Ramesh S.. "A Formal Framework for the Correct-by-construction and Verification of Distributed Time Triggered Systems". Talk or presentation, 28, August, 2007.

Abstract
In modern day automobiles, several critical vehicle functions are handled by ECS (Electronics and Control Software) applications. These are distributed, real-time, embedded systems and due to the level of criticality in their operation, they require a high-integrity development and verification process. Model-based development of such applications aims to increase the integrity of these applications through the usage of explicit models employed in clearly defined process steps leading to correct-by-construction artifacts. Ensuring consistency and correctness of models across the various design steps is crucial in model-based development methodologies. This work proposes a formal framework for this purpose. The proposed framework captures models in two stages of development - an initial abstract, centralized functional model and a subsequent model of the distributed system consisting of several ECUs (Electronic Control Units) communicating over a common bus. The proposed framework can be used both for the correct-by-construction of distributed models from the abstract functional model and for the verification of existing distributed implementations against a given functional model. We have demonstrated the utility and effectiveness of the proposed framework with two case studies - one using a conventional cruise control system and the other using a brake-by-wire sub-system.

Electronic downloads

• ramesh-berkeley-talk.pdf · · 625 kbytes

• HTML

  Ramesh S.. <a
  href="http://chess.eecs.berkeley.edu/pubs/350.html"
  ><i>A Formal Framework for the
  Correct-by-construction and Verification of Distributed Time
  Triggered Systems</i></a>, Talk or presentation,
   28, August, 2007.

• Plain text

  Ramesh S.. "A Formal Framework for the
  Correct-by-construction and Verification of Distributed Time
  Triggered Systems". Talk or presentation,  28, August,
  2007.

• BibTeX

  @presentation{S07_FormalFrameworkForCorrectbyconstructionVerification,
      author = {Ramesh S.},
      title = {A Formal Framework for the Correct-by-construction
                and Verification of Distributed Time Triggered
                Systems},
      day = {28},
      month = {August},
      year = {2007},
      abstract = {In modern day automobiles, several critical
                vehicle functions are handled by ECS (Electronics
                and Control Software) applications. These are
                distributed, real-time, embedded systems and due
                to the level of criticality in their operation,
                they require a high-integrity development and
                verification process. Model-based development of
                such applications aims to increase the integrity
                of these applications through the usage of
                explicit models employed in clearly defined
                process steps leading to correct-by-construction
                artifacts. Ensuring consistency and correctness of
                models across the various design steps is crucial
                in model-based development methodologies. This
                work proposes a formal framework for this purpose.
                The proposed framework captures models in two
                stages of development - an initial abstract,
                centralized functional model and a subsequent
                model of the distributed system consisting of
                several ECUs (Electronic Control Units)
                communicating over a common bus. The proposed
                framework can be used both for the
                correct-by-construction of distributed models from
                the abstract functional model and for the
                verification of existing distributed
                implementations against a given functional model.
                We have demonstrated the utility and effectiveness
                of the proposed framework with two case studies -
                one using a conventional cruise control system and
                the other using a brake-by-wire sub-system.},
      URL = {http://chess.eecs.berkeley.edu/pubs/350.html}
  }
  

Posted by Douglas Densmore on 10 Oct 2007.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.