Advertisement
Published in:
2007 | OriginalPaper | Chapter
How to Verify and Exploit a Refinement of Component-Based Systems
Authors : Olga Kouchnarenko, Arnaud Lanoix
Published in: Perspectives of Systems Informatics
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In order to deal with the verification of large systems, compositional approaches postpone in part the problem of combinatorial explosion during model exploration. The purpose of the work we present in this paper is to establish a compositional framework in which the verification may proceed through a refinement-based specification and a component-based verification approaches.
First, a constraint synchronised product operator enables us an automated compositional verification of a component-based system refinement relation. Secondly, safety
LTL
properties of the whole system are checked from local safety
LTL
properties of its components. The main advantage of our specification and verification approaches is that
LTL
properties are preserved through composition and refinement.