Verimag

IF

Intermediate Format and Verification Tool set

The IF Intermediate Representation based on extending communicating timed automata has been defined for being able to offer a powerful toolset offering simulation, analysis and verification facilities for different modelling languages for distributed real-time systems. The IF plays thus the role of an intermediate representation between high-level standards and verification tools. This representation is expressive enough to capture most of the functional primitives existing in standard languages such as SDL and UML (parallel execution, communication media, complex data, dynamic creation and destruction, parameterization, etc) as well as non-functional aspects related to timing, performance and scheduling.

The IF toolset includes front-ends allowing to translate different high-level modelling languages (e.g. SDL and different UML dialects) into the IF intermediate representation. Then it offers a number of backend tools for simulation and verification of IF models, and TGV allows generating test cases for a given test objective.

See also IF and IFx toolbox site

 Features

  Language

  • structuring concepts: systems consist of processes, running in parallel and communicating through message passing via communication buffers
  • communication primitives: processes may communicate either through signal exchange (directly or via signalroutes) or through shared variables
  • real-time primitives: each process may use several clocks to measure time during the execution and, in addition, transitions may be guarded with time constraints (depending on clocks) and decorated with explicit (eager, delayable, lazy) deadlines
  • open systems: the language offers the concept of open communication channel, connected to the environment, and transporting messages between it and the system
  • non-determinism: processes may be non-deterministic i.e, more than one transition may be enabled at some control state, and all situations have to be considered at execution
  • complex data types: the language provide several type constructors such as enumeration, range, array, record, abstract as well as predefined basic types in order to simplify complex data description and manipulation
  • parameterisation: it is now possible to parameterize data types (i.e, size of arrays), system configurations (i.e, number of instances), timing behavior (i.e, clock constraints)...
  • dynamic creation: the language include dynamic creation and destruction of process and signalroute (channel) instances. This makes system configuration to be dynamic, that is, the number of components running (and in turn, the number of clocks ...) may change during execution
  • structured control: the common language integrates hierachical states (to structure automata) and composed transitions basic control statements such as if-then-else and while-do are provided to structure automata transitions
  • external code integration: the common language provide a simple an elegant way to abstract complex transformations on data through the integration of external code within procedures. The external code to be provided depend on tools used i.e, an executable implementation in order to simulate and model check, or a first-order axiomatic definition in order to use it inside a prover, etc.

  Tools

  • static analysis: IF provides the dfa tool which implements classical static analysis techniques such as live variable analysis, dead-code elimination and variable elimination (backward slicing) with respect to user-defined criteria.
  • model-checking: The core component of the IF toolbox is the IF simulator allowing to explore the underlying semantic model (i.e, state graph) of an IF specification. Several exploration modes are imlemented: interactive (user-driven), random or exhaustive (breadth-first or depth-first). Partial order reductions can be applied in exhaustive- depth first search.
  • test generation: The IF simulator has been connected to the TGV test generator in the context of the AGEDIS project. See the AGEDIS web page for more details.

  Libraries

  • model: This library gives access to the abstract syntax tree (AST) of IF specifications. It can be used to implement tools operating "statically" on the specification such as translators to other languages, static analysis and optimisations at source level.
  • simulator: A simulation library providing the minimal functionality for on-the-fly state-space traversal (state representation + successors computation) is provided. It can be used to implement tools operating "dynamically" on the specifcation such as exploration tools, model-checkers, simulators, etc.

  Bugs

Report bugs here.


Contact | Site Map | Site created with SPIP 2.1.26 + AHUNTSIC [CC License]

Logged in visitors: 12 ; visits: 392535