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

• Specification%20and%20Formal%20Verification%20of%20Real%20Time%20Systems.pdf · application/pdf · 416 kbytes

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