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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Toben, T. (2007). Non-interference properties for data-type reduction of communicating systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4591 LNCS, pp. 619–638). Springer Verlag. https://doi.org/10.1007/978-3-540-73210-5_32
Mendeley helps you to discover research relevant for your work.