Resumé
The main contributions are (i) a technique for capturing the reachable states of the continuously changing state variables of the LHA as CLP constraints; (ii) a way of representing events in the LHA as constraints in CLP, along with a product construction on the CLP representation including synchronisation on shared events; (iii) a framework in which various kinds of reasoning about an LHA can be flexibly performed by combining standard CLP transformation and analysis techniques. We give experimental results to support the usefulness of the approach and argue that
we contribute to the general field of using static analysis tools for verification
| Originalsprog | Engelsk |
|---|---|
| Bogserie | Lecture Notes in Computer Science |
| Sider (fra-til) | 55-70 |
| Antal sider | 16 |
| ISSN | 0302-9743 |
| Status | Udgivet - 2009 |
| Begivenhed | Logic-Based Program Synthesis and Transformation, LOPSTR 2008 - Valencia, Spanien Varighed: 17 jul. 2008 → 18 jul. 2008 Konferencens nummer: 18th |
Konference
| Konference | Logic-Based Program Synthesis and Transformation, LOPSTR 2008 |
|---|---|
| Nummer | 18th |
| Land | Spanien |
| By | Valencia |
| Periode | 17/07/2008 → 18/07/2008 |
Bibliografisk note
Volumne: 5438Citer dette
}
Analysis of Linear Hybrid Systems in CLP. / Banda, Gourinath; Gallagher, John Patrick.
I: Lecture Notes in Computer Science, 2009, s. 55-70.Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › peer review
TY - GEN
T1 - Analysis of Linear Hybrid Systems in CLP
AU - Banda, Gourinath
AU - Gallagher, John Patrick
N1 - Volumne: 5438
PY - 2009
Y1 - 2009
N2 - In this paper we present a procedure for representing the semantics of linear hybrid automata (LHAs) as constraint logic programs (CLP); flexible and accurate analysis and verification of LHAs can then be performed using generic CLP analysis and transformation tools. LHAs provide an expressive notation for specifying real-time systems.The main contributions are (i) a technique for capturing the reachable states of the continuously changing state variables of the LHA as CLP constraints; (ii) a way of representing events in the LHA as constraints in CLP, along with a product construction on the CLP representation including synchronisation on shared events; (iii) a framework in which various kinds of reasoning about an LHA can be flexibly performed by combining standard CLP transformation and analysis techniques. We give experimental results to support the usefulness of the approach and argue thatwe contribute to the general field of using static analysis tools for verification
AB - In this paper we present a procedure for representing the semantics of linear hybrid automata (LHAs) as constraint logic programs (CLP); flexible and accurate analysis and verification of LHAs can then be performed using generic CLP analysis and transformation tools. LHAs provide an expressive notation for specifying real-time systems.The main contributions are (i) a technique for capturing the reachable states of the continuously changing state variables of the LHA as CLP constraints; (ii) a way of representing events in the LHA as constraints in CLP, along with a product construction on the CLP representation including synchronisation on shared events; (iii) a framework in which various kinds of reasoning about an LHA can be flexibly performed by combining standard CLP transformation and analysis techniques. We give experimental results to support the usefulness of the approach and argue thatwe contribute to the general field of using static analysis tools for verification
KW - Constraint Logic Programming
KW - Static analysis
KW - Linear Hybrid Systems
M3 - Conference article
SP - 55
EP - 70
JO - Lecture Notes in Computer Science
JF - Lecture Notes in Computer Science
SN - 0302-9743
ER -