@inproceedings{Tob2007,
Author = {Toben, Tobe},
Title = {Non-Interference Properties for Data-Type Reduction of Communicating Systems},

Year = {2007},
Pages = {619-638},
Month = {07},
Publisher = {Springer},
Series = {LNCS},
Edition = {4591},
type = {inproceedings},
note = {An increasing interest in \"Systems of Systems\", that is, Systems comprising a varying number of interconnected sub-systems, raises the need for automated verification techniques for dynamic process creation and a changing communication topology.},
Abstract = {An increasing interest in \"Systems of Systems\", that is, Systems comprising a varying number of interconnected sub-systems, raises the need for automated verification techniques for dynamic process creation and a changing communication topology. In previous work, we developed a verification approach that is based on finitary abstraction via Data-Type Reduction. To be effective in practice, the abstraction has to be complemented by non-trivial assumptions about valid communication behaviour, so-called non-interference lemmata. In this paper, we mechanise the generation and validation of these kind of non-interference properties by integrating ideas from communication observation and counter abstraction. We thereby provide a fully automatic procedure to substantially increase the precision of the abstraction. We explain our approach in terms of a modelling language for dynamic communication systems, and use a running example of a car platooning system to demonstrate the effectiveness of our extensions.}
}
@COMMENT{Bibtex file generated on }