Chihhong Patrick Cheng and Teale Fristoe and Edward A. Lee

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2008-41

April 19, 2008

http://www2.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},
    Year= {2008},
    Month= {Apr},
    Url= {http://www2.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://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-41.html
%F Cheng:EECS-2008-41