Library Construction for Embedded System Verification: An Experiment with JPetStore
Date Issued
2005
Date
2005
Author(s)
Cai, Lin-Zan
DOI
en-US
Abstract
RED(Region-Encoding Diagram) is an integrated symbolic TCTL model-checker/simulator for timed automata with CRD (Clock-Restriction Diagram) technology and linear hybrid automata with HRD (Hybrid-Restriction Diagram) technology. In order to share the symbolic verification technology of RED for dense-time systems and linear hybrid systems, develop more other applications on RED, and provide a more flexible and efficient way of formal method construction.
We construct the library interface of RED, REDLIB, and do an experiment with JPetStore which is a completely new implementation of Pet Store demo application written in Java. This experiment demonstrates how to use REDLIB to construct verification applications.
Subjects
驗證
模型檢驗
正規模型
函式庫
嵌入式系統
電子寵物商店
verification
model checking
formal model
library
embedded system
JPetStore
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-94-R92921105-1.pdf
Size
23.31 KB
Format
Adobe PDF
Checksum
(MD5):4f195770fc5ae2c7c7eb4a37daf0d6c4