It is widely recognised that the automated validation of complex systems can hardly be achieved without tool integration. The development of the IF-1.0 toolbox was initiated several years ago, in order to provide an open validation platform for timed asynchronous systems (such as telecommunication protocols or distributed applications, in general). The toolbox was built upon an intermediate representation language based on extended timed automata. In particular, this representation allowed us to study the semantics of real-time primitives for asynchronous systems. Currently, the toolbox contains dedicated tools on the intermediate language (such as compilers, static analysers and model-checkers) as well as front-ends to various specification languages and validation tools (academic and commercial ones). Among the dedicated tools, we focused on static analysis (such as slicing and abstraction) which are mandatory for an automated validation of complex systems. Finally, the toolbox was successfully used on several case studies, the most relevant ones being presented in. In spite of the interest of this toolbox on specific applications, it appears that some of the initial design choices, which were made to obtain a maximal efficiency, are sometimes too restrictive. In particular they may prevent its applicability to a wider context: 1. the static nature of the intermediate representation prevents the analysis of dynamic systems. More exactly, primitive operations like object (or thread) creation and destruction, which are widely and naturally used both in specification formalisms like UML or programming languages like Java, were not supported. 2. the architecture of the exploration engine allowed only the exploration of pure IF-1.0 specifications. This is too restrictive for complex system specifications which mix formal descriptions and executable code (e.g, for components already implemented and tested).
展开▼
