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.
This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Centre “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bauer, J.: Analysis of Communication Topologies by Partner Abstraction. PhD thesis, Universität des Saarlandes (2006)
Bauer, J., Schaefer, I., Toben, T., Westphal, B.: Specification and Verification of Dynamic Communication Systems. In: Goossens, K., Petrucci, L. (eds.) Proc. ACSD 2006, Turku, Finland, June 2006, IEEE, New York (2006)
Brand, D., Zafiropulo, P.: On Communicating Finite-State Machines. Journal of the Association for Computing Machinery 30(2), 323–342 (1983)
Clarke, E.M., Talupur, M., Veith, H.: Environment Abstraction for Parameterized Verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126–141. Springer, Heidelberg (2005)
Damm, W., Westphal, B.: Live and let die: LSC-based verification of UML-models. Science of Computer Programming 55(1-3), 117–159 (2005)
Frodigh, M., Johansson, P., Larsson, P.: Wireless Ad Hoc Networking: The Art of Networking without a Network. Ericsson Review, 4 (2000)
Gyuris, V., Sistla, A.P.: On-the-Fly Model Checking Under Fairness that Exploits Symmetry. Formal Methods in System Design 15(3), 217–238 (1999)
Holzmann, G.J.: The SPIN model checker: Primer and reference manual. Addison Wesley, Reading, MA (2004) HOL g 03:1 1.Ex
Hsu, A., Eskafi, F., Sachs, S., Varaiya, P.: The Design of Platoon Maneuver Protocols for IVHS. PATH Research Report UCB-ITS-PRR-91-6, Inst. of Transportation Studies, University of California (April 1991), ISSN 1055-1425
Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network Invariants in Action. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002)
Lubachevsky, B.D.: An Approach to Automating the Verification of Compact Parallel Coordination Programs I. Acta Inf. 21, 125–169 (1984)
McMillan, K.L.: A methodology for hardware verification using compositional model checking. Science of Computer Programming 37, 279–309 (2000)
Milner, R.: Communicating and Mobile Systems: The Pi Calculus. CU Press, Cambridge, MA (1999)
Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1,infty)-Counter Abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 107–133. Springer, Heidelberg (2003)
Rakow, J.: Verification of Dynamic Communication Systems. Master’s thesis, Carl von Ossietzky Universität Oldenburg (April 2006)
Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. ACM Transactions on Programming Languages and Systems, 22 (2001)
UNISIG. SUBSET 026-Chapter 3; Version 2.2.2 (SRS) (March 2002), http://www.aeif.org/ccm/default.asp
Wachter, B., Westphal, B.: The Spotlight Principle. On Combining Process-Summarising State Abstractions. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 182–198. Springer, Heidelberg (2007)
Westphal, B.: LSC Verification for UML Models with Unbounded Creation and Destruction. In: Visser, W., Cook, B., Stoller, S. (eds.) Proc. SoftMC 2005, July 2005. ENTCS, vol. 144(3), pp. 133–145. Elsevier B.V, Amsterdam (2005)
Xie, F., Browne, J.C.: Integrated State Space Reduction for Model Checking Executable Object-oriented Software System Designs. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol. 2306, pp. 64–79. Springer, Heidelberg (2002)
Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: Proc. of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pp. 25–34. ACM Press, New York (2004)
Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. ACM SIGPLAN Notices 36(3), 27–40 (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Toben, T. (2007). Non-interference Properties for Data-Type Reduction of Communicating Systems. In: Davies, J., Gibbons, J. (eds) Integrated Formal Methods. IFM 2007. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73210-5_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-73210-5_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73209-9
Online ISBN: 978-3-540-73210-5
eBook Packages: Computer ScienceComputer Science (R0)