IF-2.0

IF-2.0: A validation environment for component-based real-time systems 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. par In spite of the interest of this toolbox on specifie 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: par -- 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. par -- 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). par This situation motivated the extension of the IF-1.0 intermediate representation and, in turn, to re-consider the architecture of the exploration engine.


References in zbMATH (referenced in 46 articles , 2 standard articles )

Showing results 21 to 40 of 46.
Sorted by year (citations)
  1. Maler, Oded; Batt, Grégory: Approximating continuous systems by timed automata (2008)
  2. Ober, Iulian; Graf, Susanne; Yushtein, Yuri; Ober, Ileana: Timing analysis and validation with UML: the case of the embedded MARS bus manager (2008) ioport
  3. Srba, Jiří: Comparing the expressiveness of timed automata and timed extensions of Petri nets (2008)
  4. Bazilio, Carlos; Haeusler, Edward Hermann; Endler, Markus: Language-oriented formal analysis: a case study on protocols and distributed systems (2007)
  5. Ölveczky, Peter Csaba; Meseguer, José: Recent advances in real-time Maude (2007)
  6. Ölveczky, Peter Csaba; Meseguer, José: Semantics and pragmatics of real-time maude (2007)
  7. Abdeddaïm, Yasmina; Asarin, Eugene; Maler, Oded: Scheduling with timed automata (2006)
  8. Graf, Susanne; Haugen, Oystein; Ober, Ileana; Selic, Bran: Preface of “Specification and validation of real time and embedded systems in UML” (2006) ioport
  9. Graf, Susanne; Ober, Ileana; Ober, Iulian: A real-time profile for UML (2006) ioport
  10. Madl, Gabor; Abdelwahed, Sherif; Schmidt, Douglas C.: Verifying distributed real-time properties of embedded systems via graph transformations and model checking (2006)
  11. Niebert, Peter; Qu, Hongyang: The implementation of Mazurkiewicz traces in POEM (2006)
  12. Ober, Iulian; Graf, Susanne; Ober, Ileana: Validating timed UML models by simulation and verification (2006) ioport
  13. Ölveczky, Peter Csaba; Meseguer, José; Talcott, Carolyn L.: Specification and analysis of the AER/NCA active network protocol suite in real-time Maude (2006)
  14. D’Argenio, Pedro R.; Gebremichael, Biniam: The coarsest congruence for timed automata with deadlines contained in bisimulation (2005)
  15. Iosif, Radu; Dwyer, Matthew B.; Hatcliff, John: Translating Java for multiple model checkers: The Bandera back-end (2005)
  16. Jard, Claude; Jéron, Thierry: TGV: theory, principles and algorithms (2005) ioport
  17. Jard, Claude; Jéron, Thierry: TGV: theory, principles and algorithms: a tool for the automatic synthesisof conformance test cases for non-deterministic reactive systems (2005) ioport
  18. Loghi, Mirko; Margaria, Tiziana; Pravadelli, Graziano; Steffen, Bernhard: Dynamic and formal verification of embedded systems: A comparative survey (2005)
  19. Ben Salah, Ramzi; Bozga, Marius; Maler, Oded: On timing analysis of combinational circuits (2004)
  20. Bozga, Marius; Graf, Susanne; Mounier, Laurent; Ober, Iulian: IF validation environment tutorial (2004)