*banner
 

Specification and Formal Verification of Real Time Systems under Ptolemy II
Chihhong Cheng, Edward A. Lee

Citation
Chihhong Cheng, Edward A. Lee. "Specification and Formal Verification of Real Time Systems under Ptolemy II". Talk or presentation, 21, February, 2008; Poster presented at the 2008 Berkeley EECS Annual Research Symposium.

Abstract
To overcome the existing challenge in the design of embedded software, mediating the gap between design facilitation and verification complication is important. Existing theories and practices in verification are powerful, but when applying formal techniques, the use of detailed description of mathematical models greatly increases the burden of system designers. Detailed and complex mathematical models used for verification should be hidden; construction of such models may be time consuming and error prone. In Ptolemy II, we try to solve this problem by providing an automatic mapping from higher level components (actors) commonly used to lower level mathematical models; the conversion preserves the behavior semantics. With this methodology, the productivity of designers as well as the correctness of designs can be maintained simultaneously.

Electronic downloads

Citation formats  
  • HTML
    Chihhong Cheng, Edward A. Lee. <a
    href="http://chess.eecs.berkeley.edu/pubs/392.html"
    ><i>Specification and Formal Verification of Real
    Time Systems under Ptolemy II</i></a>, Talk or
    presentation,  21, February, 2008; Poster presented at the
    2008
    <a
    href="http://www.eecs.berkeley.edu/bears/"
    >Berkeley EECS Annual  Research Symposium</a>.
  • Plain text
    Chihhong Cheng, Edward A. Lee. "Specification and
    Formal Verification of Real Time Systems under Ptolemy
    II". Talk or presentation,  21, February, 2008; Poster
    presented at the 2008
    <a
    href="http://www.eecs.berkeley.edu/bears/"
    >Berkeley EECS Annual  Research Symposium</a>.
  • BibTeX
    @presentation{ChengLee08_SpecificationFormalVerificationOfRealTimeSystemsUnder,
        author = {Chihhong Cheng and Edward A. Lee},
        title = {Specification and Formal Verification of Real Time
                  Systems under Ptolemy II},
        day = {21},
        month = {February},
        year = {2008},
        note = {Poster presented at the 2008
    <a
                  href="http://www.eecs.berkeley.edu/bears/"
                  >Berkeley EECS Annual  Research Symposium</a>.},
        abstract = {To overcome the existing challenge in the design
                  of embedded software, mediating the gap between
                  design facilitation and verification complication
                  is important. Existing theories and practices in
                  verification are powerful, but when applying
                  formal techniques, the use of detailed description
                  of mathematical models greatly increases the
                  burden of system designers. Detailed and complex
                  mathematical models used for verification should
                  be hidden; construction of such models may be time
                  consuming and error prone. In Ptolemy II, we try
                  to solve this problem by providing an automatic
                  mapping from higher level components (actors)
                  commonly used to lower level mathematical models;
                  the conversion preserves the behavior semantics.
                  With this methodology, the productivity of
                  designers as well as the correctness of designs
                  can be maintained simultaneously.},
        URL = {http://chess.eecs.berkeley.edu/pubs/392.html}
    }
    

Posted by Chihhong Cheng, Dr. ner. nat. on 22 Feb 2008.
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