Title
Monitoring of Probabilistic Timed Property Sequence Charts
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 Zhang115310.70
Wenrui Li2588.98
Dingsheng Wan3978.76
Lars Grunske4150573.07