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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Metzler, B. (2007). Decomposing integrated specifications for verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4591 LNCS, pp. 459–479). Springer Verlag. https://doi.org/10.1007/978-3-540-73210-5_24
Mendeley helps you to discover research relevant for your work.