Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Applied Verification: The Ptolemy Approach

Chihhong Patrick Cheng, Teale Fristoe and Edward A. Lee

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2008-41
April 19, 2008

http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-41.pdf

This paper addresses the difficulty that designers of embedded software systems face when doing formal verification. Existing theories and practices in verification are powerful, but when applying formal techniques, the use of detailed mathematical model descriptions in verification greatly increase the burden on system designers; construction of such models may be time consuming and error prone. We lay the groundwork for solving this problem by providing a mapping from actor models to mathematical models suitable for verification; the conversion is automatic with minimal human intervention. Meanwhile, the interactions between the verification model and its environment can guide us in designing how the implementation model interprets the raw data from sensors and to actuators, allowing us to reuse the verification model as the basis of its implementation model. Following these strategies, the productivity of designers and the correctness of designs can be maintained simultaneously.


BibTeX citation:

@techreport{Cheng:EECS-2008-41,
    Author = {Cheng, Chihhong Patrick and Fristoe, Teale and Lee, Edward A.},
    Title = {Applied Verification: The Ptolemy Approach},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2008},
    Month = {Apr},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-41.html},
    Number = {UCB/EECS-2008-41},
    Abstract = {This paper addresses the difficulty that designers of embedded software systems face when doing formal verification. Existing theories and practices in verification are powerful, but when applying formal techniques, the use of detailed mathematical model descriptions in verification greatly increase the burden on system designers; construction of such models may be time consuming and error prone. We lay the groundwork for solving this problem by providing a mapping from actor models to mathematical models suitable for verification; the conversion is automatic with minimal human intervention. Meanwhile, the interactions between the verification model and its environment can guide us in designing how the implementation model interprets the raw data from sensors and to actuators, allowing us to reuse the verification model as the basis of its implementation model. Following these strategies, the productivity of designers and the correctness of designs can be maintained simultaneously.}
}

EndNote citation:

%0 Report
%A Cheng, Chihhong Patrick
%A Fristoe, Teale
%A Lee, Edward A.
%T Applied Verification: The Ptolemy Approach
%I EECS Department, University of California, Berkeley
%D 2008
%8 April 19
%@ UCB/EECS-2008-41
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-41.html
%F Cheng:EECS-2008-41