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 40 articles , 2 standard articles )

Showing results 1 to 20 of 40.
Sorted by year (citations)

1 2 next

  1. Nepomniaschy, V.; Bodin, E.; Veretnov, S.: The language dynamic-real and its application for verification of SDL-specified distributed systems (2015)
  2. Byg, Joakim; Jacobsen, Morten; Jacobsen, Lasse; Jørgensen, Kenneth Yrke; Møller, Mikael Harkjær; Srba, Jiří: TCTL-preserving translations from timed-arc Petri nets to networks of timed automata (2014)
  3. Gómez, Rodolfo: Model-checking timed automata with deadlines with Uppaal (2013)
  4. Van Goethem, S.; Jacquet, J.-M.; Brim, L.; Šafránek, D.: Timed modelling of gene networks with arbitrarily precise expression discretization (2013)
  5. Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
  6. Kempf, Jean-Francois; Bozga, Marius; Maler, Oded: Performance evaluation of schedulers in a probabilistic setting (2011)
  7. Wang, Farn; Yao, Li-Wei; Yang, Ya-Lan: Efficient verification of distributed real-time systems with broadcasting behaviors (2011)
  8. Bartocci, Ezio; Corradini, Flavio; Merelli, Emanuela; Tesei, Luca: Detecting synchronisation of biological oscillators by model checking (2010)
  9. Lang, Frédéric; Salaün, Gwen; Hérilier, Rémi; Kramer, Jeff; Magee, Jeff: Translating FSP into LOTOS and networks of automata (2010)
  10. Malinowski, Janusz; Niebert, Peter: SAT based bounded model checking with partial order semantics for timed automata (2010)
  11. van Beek, D.A.; Cuijpers, P.J.L.; Markovski, J.; Nadales Agut, D.E.; Rooda, J.E.: Reconciling urgency and variable abstraction in a hybrid compositional setting (2010)
  12. Alexander, Michael (ed.); Gardner, William (ed.): Process algebra for parallel and distributed processing. (2009)
  13. Gómez, Rodolfo: A compositional translation of timed automata with deadlines to Uppaal timed automata (2009)
  14. Jaghoori, Mohammad Mahdi; de Boer, Frank S.; Chothia, Tom; Sirjani, Marjan: Schedulability of asynchronous real-time concurrent objects (2009)
  15. Ölveczky, Peter Csaba; Thorvaldsen, Stian: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude (2009)
  16. Hooman, Jozef; Kugler, Hillel; Ober, Iulian; Votintseva, Anjelika; Yushtein, Yuri: Supporting UML-based development of embedded systems by formal techniques (2008)
  17. Maler, Oded; Batt, Grégory: Approximating continuous systems by timed automata (2008)
  18. Ober, Iulian; Graf, Susanne; Yushtein, Yuri; Ober, Ileana: Timing analysis and validation with UML: the case of the embedded MARS bus manager (2008)
  19. Srba, Jiří: Comparing the expressiveness of timed automata and timed extensions of Petri nets (2008)
  20. Ölveczky, Peter Csaba; Meseguer, José: Semantics and pragmatics of real-time maude (2007)

1 2 next