CIF 3

About

TU/e logo SE logo CIF 3 logo

The CIF 3 language

The CIF 3 language features the following concepts:

  • Automata with synchronizing events.
  • Several different types of automata (plants, requirements, etc).
  • Automaton definition/instantiation.
  • Grouping of automata.
  • Multiple initial locations per automaton.
  • Marker predicates, which is a generalization of marker states.
  • Controllable/uncontrollable events.
  • Automatic alphabet resolving (it is barely ever needed to manually specify the alphabet).
  • Automata can specify a set of monitor events, which they then don’t block.
  • Edges with events, guards, updates, and urgency. Conditional updates, multi-assignments, and projection at the left hand side of assignments are supported as well.
  • State (exclusion) invariants, which are predicates that always hold.
  • State/event exclusion invariants, which are global properties that can disable events in certain states.
  • Discrete variables, which may only be modified locally (that is, by the automaton that declares it), but may be read globally.
  • Initialization predicates, and non-deterministic initialization of discrete variables.
  • Algebraic variables, which are shortcuts for expressions.
  • Continuous variables with explicit equations for their derivatives.
  • Constants.
  • Enumerations.
  • Type definitions.
  • Various types, including booleans, integers (both ranged and unranged), reals, strings, lists, sets, dictionaries, functions, tuples, distributions, etc. The language also has a rich expression syntax.
  • Over a dozen stochastic distributions that support sampling.
  • Events can optionally have data types, turning them into channels. Channels allow for point-to-point communication, with exactly one sender and one receiver. Channels may be further restricted by synchronization.
  • Internal user-defined functions, which are fully defined in the CIF specification. External user-defined functions, for which the header is defined in the CIF specification, while the implementation resides somewhere else.

History

CIF 3 is the next big new version of CIF, after CIF 1, and CIF 2, which were both developed in European projects, including among others HYCON, HYCON2, Multiform, and C4C. CIF 3 was redesigned from scratch. It has much simpler syntax and semantics. Furthermore, CIF 3 integrates concepts used for supervisory controller synthesis, directly in the language. The third and final major improvement of CIF 3 over CIF 2 is the tooling, which is much much faster, and provides much better user feedback.

Publications

Key CIF 3 publications:

  • D.A. van Beek, W.J. Fokkink, D. Hendriks, A. Hofkamp, J. Markovski, J.M. van de Mortel-Fronczak, and M.A. Reniers
    E. Ábrahám and K. Havelund (Eds.): TACAS 2014, LNCS 8413, pages 575-580, 2014
    Springer-Verlag Berlin Heidelberg 2014

Key CIF 2 publications:

Key CIF 1 publications: