Abstract | ||
---|---|---|
Run-time monitoring is an important technique to detect erroneous run-time behaviors. Several techniques have been proposed to automatically generate monitors from specification languages to check temporal and real-time properties. However, monitoring of probabilistic properties still requires manual generation. To overcome this problem, we define a formal property specification language called Probabilistic Timed Property Sequence Chart (PTPSC). PTPSC is a probabilistic and timed extension of the existing scenario-based specification formalism Property Sequence Chart (PSC). We have defined a formal grammar-based syntax and have implemented a syntax-directed translator that can automatically generate a probabilistic monitor which combines timed B”uchi automata and a sequential statistical hypothesis test process. We validate the generated monitors with a set of experiments performed with our tool WS-PSC Monitor. Copyright © 2011 John Wiley & Sons, Ltd. |
Year | DOI | Venue |
---|---|---|
2011 | 10.1002/spe.1038 | Softw., Pract. Exper. |
Keywords | DocType | Volume |
formal property specification language,Probabilistic Timed Property Sequence,existing scenario-based specification formalism,formal grammar-based syntax,Run-time monitoring,specification language,probabilistic monitor,probabilistic property,John Wiley,Property Sequence Chart | Journal | 41 |
Issue | ISSN | Citations |
7 | 0038-0644 | 20 |
PageRank | References | Authors |
0.81 | 33 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Pengcheng Zhang | 1 | 153 | 10.70 |
Wenrui Li | 2 | 58 | 8.98 |
Dingsheng Wan | 3 | 97 | 8.76 |
Lars Grunske | 4 | 1505 | 73.07 |