Analysis of Linear Hybrid Systems in CLP

Gourinath Banda; John Patrick Gallagher

Analysis of Linear Hybrid Systems in CLP

Programmering, logik og intelligente systemer

Publikation: Bidrag til tidsskrift › Konferenceartikel › peer review

Abstract

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 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/Område	Spanien
By	Valencia
Periode	17/07/2008 → 18/07/2008

Bibliografisk note

Volumne: 5438

Link til dokument

PaperForlagets udgivne version, 368 KB

Citer dette

@inproceedings{97f7589016cd11de8600000ea68e967b,

title = "Analysis of Linear Hybrid Systems in CLP",

abstract = "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",

keywords = "Constraint Logic Programming, Static analysis, Linear Hybrid Systems",

author = "Gourinath Banda and Gallagher, {John Patrick}",

note = "Volumne: 5438; null ; Conference date: 17-07-2008 Through 18-07-2008",

year = "2009",

language = "English",

pages = "55--70",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Physica-Verlag",

}

TY - GEN

T1 - Analysis of Linear Hybrid Systems in CLP

AU - Banda, Gourinath

AU - Gallagher, John Patrick

N1 - Conference code: 18th

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

Y2 - 17 July 2008 through 18 July 2008

ER -