Symbolic invariant verification for systems with dynamic structural adaptation

ABSTRACT

The next generation of networked mechatronic systems will be characterized by complex coordination and structural adaptation at run-time. Crucial safety properties have to be guaranteed for all potential structural configurations. Testing cannot provide safety guarantees, while current model checking and theorem proving techniques do not scale for such systems. We present a verification technique for arbitrarily large multi-agent systems from the mechatronic domain, featuring complex coordination and structural adaptation. We overcome the limitations of existing techniques by exploiting the local character of structural safety properties. The system state is modeled as a graph, system transitions are modeled as rule applications in a graph transformation system, and safety properties of the system are encoded as inductive invariants (permitting the verification of infinite state systems). We developed a symbolic verification procedure that allows us to perform the computation on an efficient BDD-based graph manipulation engine, and we report performance results for several examples.

REFERENCES

• 1: Paolo Baldan , Andrea Corradini , Barbara König, A Static Analysis Technique for Graph Transformation Systems, Proceedings of the 12th International Conference on Concurrency Theory, p.381-395, August 20-25, 2001
• 2: P. Baldan, B. König, and A. Rensink. Graph grammar verification through abstraction (summary 2). Proc. Dagstuhl Seminar 04241, 2005.
• 3: Luciano Baresi , Reiko Heckel , Sebastian Thöne , Dániel Varró, Modeling and validation of service-oriented architectures: application vs. style, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 4: Dirk Beyer , Andreas Noack , Claus Lewerentz, Efficient Relational Calculation for Software Analysis, IEEE Transactions on Software Engineering, v.31 n.2, p.137-149, February 2005 [doi>10.1109/TSE.2005.23]
• 5: Ramesh Bharadwaj , Steve Sims, Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.378-394, March 25-April 02, 2000
• 6: D. Bradley, D. Seward, D. Dawson, and S. Burge. Mechatronics. Stanley Thornes, 2000.
• 7: S. Burmester, H. Giese, and M. Tichy. Model-driven development of reconfigurable mechatronic systems with mechatronic UML. In Model Driven Architecture: Foundations and Applications, LNCS 3599, pages 47--61. Springer, 2005.
• 8: M. Caporuscio, P. Inverardi, and P. Pelliccione. Formal analysis of architectural patterns. In Proc. EWSA, LNCS 3047, pages 10--24. Springer, 2004.
• 9: M. Charpentier. Composing invariants. In Proc. FME, LNCS 2805, pages 401--421. Springer, 2003.
• 10: Marcelo F. Frias , Juan P. Galeotti , Carlos G. López Pombo , Nazareno M. Aguirre, DynAlloy: upgrading alloy with actions, Proceedings of the 27th international conference on Software engineering, p.442-451, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062535]
• 11: Holger Giese , Sven Burmester , Wilhelm Schäfer , Oliver Oberschelp, Modular design and verification of component-based mechatronic systems with online-reconfiguration, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 12: H. Giese and D. Schilling. Towards the automatic verification of inductive invariants for infinite state UML models. Technical Report tr-ri-04-252, University of Paderborn, Germany, 2004.
• 13: Holger Giese , Matthias Tichy , Sven Burmester , Stephan Flake, Towards the compositional verification of real-time UML designs, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 14: R. Heckel, J. Küster, and G. Taentzer. Towards automatic translation of UML models into semantic domains. In Proc. AGT, pages 11--22, 2002.
• 15: R. Heckel and A. Wagner. Ensuring consistency of conditional graph rewriting --- a constructive approach ENTCS, 2, 1995.
• 16: Daniel Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.2, p.256-290, April 2002 [doi>10.1145/505145.505149]
• 17: F. Klein and H. Giese. Separation of concerns for mechatronic multi-agent systems through dynamic communities. In SELMAS III, LNCS 3390, pages 272--289. Springer, 2005.
• 18: Hans J. Köhler , Ulrich Nickel , Jörg Niere , Albert Zündorf, Integrating UML diagrams for production control systems, Proceedings of the 22nd international conference on Software engineering, p.241-251, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337207]
• 19: David J. Musliner , Robert P. Goldman , Michael J. Pelican , Kurt D. Krebsbach, Self-Adaptive Software for Hard Real-Time Environments, IEEE Intelligent Systems, v.14 n.4, p.23-29, July 1999 [doi>10.1109/5254.784081]
• 20: P. Ölveczky and J. Meseguer. Specification and analysis of real-time systems using Real-Time Maude. In Proc. FASE, LNCS 2984, pages 354--358. Springer, 2004.
• 21: A. Rensink. Towards model checking graph grammars. In Proc. AVoCS, pages 150--160. University of Southampton, 2003.
• 22: Grzegorz Rozenberg, Handbook of graph grammars and computing by graph transformation: volume I. foundations, World Scientific Publishing Co., Inc., River Edge, NJ, 1997
• 23: Janos Sztipanovits , Gabor Karsai , Ted Bapty, Self-adaptive software for signal processing, Communications of the ACM, v.41 n.5, p.66-73, May 1998 [doi>10.1145/274946.274958]
• 24: D. Varró. Automated formal verification of visual modeling languages by model checking. Software and System Modeling, 3(2):85--113, 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Domain-specific architectures
      D.2.2 Design Tools and Techniques
          Subjects: Computer-aided software engineering (CASE)

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants

General Terms:
Design, Reliability, Verification

Keywords:
embedded systems, gormal verification, hraph transformation systems, mechatronics, structural invariants, symbolic algorithms, transition invariants