Compositional Verification of Quantitative Properties of Statecharts.
Saved in:
| 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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 44627622 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Compositional Verification of Quantitative Properties of Statecharts. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22LEVI%2C+FRANCESCA%22">LEVI, FRANCESCA</searchLink><relatesTo>1</relatesTo><i> levifran@di.unipi.it</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Logic+%26+Computation%22">Journal of Logic & Computation</searchLink>. Dec2001, Vol. 11 Issue 6, p829-878. 50p. 3 Diagrams, 4 Charts. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Statecharts+%28Computer+science%29%22">Statecharts (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Semantics%22">Semantics</searchLink><br /><searchLink fieldCode="DE" term="%22Charts%2C+diagrams%2C+etc%2E%22">Charts, diagrams, etc.</searchLink><br /><searchLink fieldCode="DE" term="%22Parallel+processing%22">Parallel processing</searchLink><br /><searchLink fieldCode="DE" term="%22Logic%22">Logic</searchLink><br /><searchLink fieldCode="DE" term="%22Language+%26+languages%22">Language & languages</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=44627622 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1093/logcom/11.6.829 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 50 StartPage: 829 Subjects: – SubjectFull: Statecharts (Computer science) Type: general – SubjectFull: Semantics Type: general – SubjectFull: Charts, diagrams, etc. Type: general – SubjectFull: Parallel processing Type: general – SubjectFull: Logic Type: general – SubjectFull: Language & languages Type: general Titles: – TitleFull: Compositional Verification of Quantitative Properties of Statecharts. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: LEVI, FRANCESCA IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 12 Text: Dec2001 Type: published Y: 2001 Identifiers: – Type: issn-print Value: 0955792X Numbering: – Type: volume Value: 11 – Type: issue Value: 6 Titles: – TitleFull: Journal of Logic & Computation Type: main |
| ResultId | 1 |
