Applications of Hierarchical Reasoning in the Verification of Complex Systems | Zendy

Swen Jacobs | Zendy; Viorica Sofronie-Stokkermans | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Applications of Hierarchical Reasoning in the Verification of Complex Systems

Author(s) -

Swen Jacobs,

Viorica Sofronie-Stokkermans

Publication year - 2007

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2006.11.038

Subject(s) - model checking , satisfiability , bounded function , computer science , theoretical computer science , base (topology) , boolean satisfiability problem , abstraction model checking , algorithm , formal verification , programming language , mathematics , mathematical analysis

In this paper we show how hierarchical reasoning can be used to verify properties of complex systems. Chains of local theory extensions are used to model a case study taken from the European Train Control System (ETCS) standard, but considerably simplified. We show how testing invariants and bounded model checking (for safety properties expressed by universally quantified formulae, depending on certain parameters of the systems) can automatically be reduced to checking satisfiability of ground formulae over a base theory

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research