*banner
 

A Formal Framework for the Correct-by-construction and Verification of Distributed Time Triggered Systems
Ramesh S.

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

Citation formats  
  • 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess