Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Decomposing Integrated Specifications for Verification
verfasst von : Björn Metzler
Erschienen in: Integrated Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Integrated formal specifications are intrinsically difficult to (automatically) verify due to the combination of complex data and behaviour. In this paper, we present a method for
decomposing
specifications into several smaller parts which can be independently verified. Verification results can then be combined to make a global result according to the original specification.
Instead of relying on an
a priori
given structure of the system such as a parallel composition of components, we compute the decomposition by ourselves using the technique of
slicing
. With less effort, significant properties can be verified for the resulting specification parts and be applied to the full specification. We prove correctness of our method and exemplify it according to a specification from the rail domain.