A Compositional Framework for Formally Verifying Modular Systems | Zendy

Carlo A. Furia | Zendy; Matteo Rossi | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Compositional Framework for Formally Verifying Modular Systems

Author(s) -

Carlo A. Furia,

Matteo Rossi

Publication year - 2005

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.2004.02.076

Subject(s) - modular design , computer science , automated theorem proving , gas meter prover , rule of inference , property (philosophy) , simple (philosophy) , inference , theoretical computer science , programming language , proof assistant , mathematical proof , mathematics , artificial intelligence , philosophy , geometry , epistemology

We present a tool-supported framework for proving that the composition of the behaviors of the separate parts of a complex system ensures a desired global property of the overall system. A compositional inference rule is formally introduced and encoded in the logic of the PVS theorem prover. Methodological considerations on the usage of the inference rule are presented, and the framework is then used to prove a meaningful property of a simple, but significant, control system

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