About

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:

• CIF 3: Model-Based Engineering of Supervisory Controllers

  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:

• Syntax and Semantics of the Compositional Interchange Format for Hybrid Systems

  D.E. Nadales Agut, D.A. van Beek, and J.E. Rooda

  Journal of Logic and Algebraic Programming, vol 82 (nr 1), pages 1-52, 2013

Key CIF 1 publications:

• Foundations of a compositional interchange format for hybrid systems

  D.A. van Beek, M.A. Reniers, R.R.H. Schiffelers, and J.E. Rooda

  A. Bemporad, A. Bicchi, and G. Buttazzo (Eds.): HSCC 2007, LNCS 4416, pages 587-600, 2007

  Springer-Verlag Berlin Heidelberg 2007

Version r9682. Copyright © 2012-2016, Eindhoven University of Technology. Created using Sphinx 1.2.2.