Analysis of Linear Hybrid Systems in CLP

Gourinath Banda, John Patrick Gallagher

Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

Resumé

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
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Sider (fra-til)55-70
Antal sider16
ISSN0302-9743
StatusUdgivet - 2009
BegivenhedLogic-Based Program Synthesis and Transformation,  LOPSTR 2008 - Valencia, Spanien
Varighed: 17 jul. 200818 jul. 2008
Konferencens nummer: 18th

Konference

KonferenceLogic-Based Program Synthesis and Transformation,  LOPSTR 2008
Nummer18th
LandSpanien
ByValencia
Periode17/07/200818/07/2008

Bibliografisk note

Volumne: 5438

Emneord

    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",
    year = "2009",
    language = "English",
    pages = "55--70",
    journal = "Lecture Notes in Computer Science",
    issn = "0302-9743",
    publisher = "Physica-Verlag",

    }

    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 tidsskriftKonferenceartikelForskningpeer 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 -