z-logo
Premium
Modular formal verification of specifications of concurrent systems
Author(s) -
Gradara Sara,
Santone Antonella,
Vaglini Gigliola,
Villani Maria Luisa
Publication year - 2008
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.371
Subject(s) - modular design , component (thermodynamics) , computer science , formal methods , process (computing) , programming language , focus (optics) , formal verification , software engineering , physics , optics , thermodynamics
Abstract In this paper, we propose a bottom‐up approach for the verification of systems with modular structure: we prove that when the modules are composed in specific ways, the complete software system verifies a composition of the properties each component does. We focus on the process of upgrading systems with new functionalities, where the validity of old requirements needs to be ensured, but also an understanding of the new properties the upgraded system would enjoy is useful. In this work, we assume each component to be specified by a CCS process, and the properties to be expressed by selective mu‐calculus formulae. Copyright © 2007 John Wiley & Sons, Ltd.

This content is not available in your region!

Continue researching here.

Having issues? You can contact us here