Automatic Verification of the Control Flow Model for Effective Embedded Software Design


The KIPS Transactions:PartA, Vol. 12, No. 7, pp. 563-570, Dec. 2005
10.3745/KIPSTA.2005.12.7.563,   PDF Download:

Abstract

Hardware and software codesign framework called PeaCE(Ptolemy extension as a Codesign Environment) allows to express both data flow and control flow. To formally verify an fFSM specification which expresses control flow in PeaCE, the step semantics of the model was defined. In this paper, we introduce the automatic verification tool developed by formal semantics of previous work. This tool uses the SMV as inner model checker and, through our tool, users can formally verify some important bugs such as race condition, ambiguous transition, and circulartransition without directly writing logical formulae.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
S. C. Park, G. H. Kwon, S. H. Ha, "Automatic Verification of the Control Flow Model for Effective Embedded Software Design," The KIPS Transactions:PartA, vol. 12, no. 7, pp. 563-570, 2005. DOI: 10.3745/KIPSTA.2005.12.7.563.

[ACM Style]
Sa Choun Park, Gi Hwon Kwon, and Soon Hoi Ha. 2005. Automatic Verification of the Control Flow Model for Effective Embedded Software Design. The KIPS Transactions:PartA, 12, 7, (2005), 563-570. DOI: 10.3745/KIPSTA.2005.12.7.563.