Bibliographic Details
| Title: |
Compositional Verification of Quantitative Properties of Statecharts. |
| Authors: |
LEVI, FRANCESCA1 levifran@di.unipi.it |
| Source: |
Journal of Logic & Computation. Dec2001, Vol. 11 Issue 6, p829-878. 50p. 3 Diagrams, 4 Charts. |
| Subjects: |
Statecharts (Computer science), Semantics, Charts, diagrams, etc., Parallel processing, Logic, Language & languages |
| Abstract: |
In this paper we propose a process language JSP which abstractly models timed statecharts with minimal and maximal delays associated to transitions. Statecharts processes are equipped with a labelled transition system semantics that combines the basic principles of the semantics of Pnueli and Shalev with discrete time. Furthermore, we propose a compositional proof system to check quantitative temporal properties of statecharts processes. Properties are expressed in a discrete extension of µ‐calculus with reset over clocks and clock constraints. The proof system is sound in general and it is complete for the class of regular processes (including processes corresponding to statecharts). [ABSTRACT FROM PUBLISHER] |
|
Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
