Basil Becker
Dirk Beyer
Holger Giese
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.
- P. Baldan, A. Corradini, and B. König. A static analysis technique for graph transformation systems. In Proc. CONCUR, LNCS 2154, pages 381--395. Springer, 2001.]] Google Scholar
Digital Library
- P. Baldan, B. König, and A. Rensink. Graph grammar verification through abstraction (summary 2). Proc. Dagstuhl Seminar 04241, 2005.]]Google Scholar
- L. Baresi, R. Heckel, S. Thöne, and D. Varró. Modeling and validation of service-oriented architectures: Application vs. style. In Proc. ESEC/FSE, pages 68--77. ACM, 2003.]] Google ScholarDigital Library
- D. Beyer, A. Noack, and C. Lewerentz. Efficient relational calculation for software analysis. IEEE Trans. on Software Engineering, 31(2):137--149, 2005.]] Google ScholarDigital Library
- R. Bharadwaj and S. Sims. Salsa: Combining constraint solvers with BDDs for automatic invariant checking. In Proc. TACAS, LNCS 1785, pages 378--394. Springer, 2000.]] Google ScholarDigital Library
- D. Bradley, D. Seward, D. Dawson, and S. Burge. Mechatronics. Stanley Thornes, 2000.]]Google Scholar
- 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.]] Google ScholarDigital Library
- M. Caporuscio, P. Inverardi, and P. Pelliccione. Formal analysis of architectural patterns. In Proc. EWSA, LNCS 3047, pages 10--24. Springer, 2004.]]Google ScholarCross Ref
- M. Charpentier. Composing invariants. In Proc. FME, LNCS 2805, pages 401--421. Springer, 2003.]]Google ScholarCross Ref
- M. F. Frias, J. P. Galeotti, C. L. Pombo, and N. Aguirre. DynAlloy: Upgrading Alloy with actions. In Proc. ICSE, pages 442--451. ACM, 2005.]] Google ScholarDigital Library
- H. Giese, S. Burmester, W. Schäfer, and O. Oberschelp. Modular design and verification of component-based mechatronic systems with online reconfiguration. In Proc. FSE, pages 179--188. ACM, 2004.]] Google ScholarDigital Library
- 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.]]Google Scholar
- H. Giese, M. Tichy, S. Burmester, W. Schäfer, and S. Flake. Towards the compositional verification of real-time UML designs. In Proc. ESEC/FSE, pages 38--47. ACM, 2003.]] Google ScholarDigital Library
- R. Heckel, J. Küster, and G. Taentzer. Towards automatic translation of UML models into semantic domains. In Proc. AGT, pages 11--22, 2002.]]Google Scholar
- R. Heckel and A. Wagner. Ensuring consistency of conditional graph rewriting --- a constructive approach ENTCS, 2, 1995.]]Google Scholar
- D. Jackson. Alloy: A lightweight object modelling notation. ACM Trans. Software Engineering and Methodology, 11(2):256--290, 2002.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- H. Köhler, U. Nickel, J. Niere, and A. Zündorf. Integrating UML diagrams for production control systems. In Proc. ICSE, pages 241--251. ACM, 2000.]] Google ScholarDigital Library
- D. Musliner, R. Goldman, M. Pelican, and K. Krebsbach. Self-adaptive software for hard real-time environments. IEEE Intelligent Systems, 14(4), 1999.]] Google ScholarDigital Library
- 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.]]Google ScholarCross Ref
- A. Rensink. Towards model checking graph grammars. In Proc. AVoCS, pages 150--160. University of Southampton, 2003.]]Google Scholar
- G. Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, volume 1. World Scientific Pub Co, 1997.]] Google ScholarDigital Library
- J. Sztipanovits, G. Karsai, and T. Bapty. Self-adaptive software for signal processing Commun. ACM, 41(5):66--73, 1998.]] Google ScholarDigital Library
- D. Varró. Automated formal verification of visual modeling languages by model checking. Software and System Modeling, 3(2):85--113, 2004.]]Google ScholarDigital Library
Index Terms
- Symbolic invariant verification for systems with dynamic structural adaptation
Recommendations
A classification of symbolic transition systems
We define five increasingly comprehensive classes of infinite-state systems, called STS1--STS5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems.STS1 These are the systems with finite ...
Automatic Symbolic Verification of Embedded Systems
We present a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as Hybrid Automata communicating machines with finite control and real-valued variables that represent ...
HW/SW co-verification of embedded systems using bounded model checking
GLSVLSI '06: Proceedings of the 16th ACM Great Lakes symposium on VLSIToday, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the functional correctness. But in embedded system design the integration of software components becomes ...
Comments