User Tools

Site Tools


cif:start

This is an old revision of the document!


CIF: The Compositional Interchange Format for Hybrid Systems

New CIF 3 toolset available

For all new developments, please use the CIF 3 toolset, available via the CIF 3 website at http://cif.mn.wtb.tue.nl.

Introduction

In the European network of excellence HYCON in work package 3: Tool Integration, the Compositional Interchange Format (CIF) has been defined. The purpose of the Compositional Interchange Format is to establish inter-operability of a wide range of tools by means of model transformations to and from the CIF, as shown in the figure. Using the CIF as intermediate, the implementation of many bi-lateral translators between specific formalisms can be avoided.

Multiple model transformations using the CIF

The figure below gives an overview of work on the CIF in different projects, showing each project in a different color. Work on the CIF in HYCON has been continued in the EU FP7 project Multiform, where bidirectional transformations between the CIF and several languages/tools are developed, and in HYCON2. In the EU FP7 project C4C, work on the CIF is mainly on compositional verification. The CIF is used in several industrial projects. Two examples, one from the Twins, and one from the Darwin project, are presented in italics in the figure below.

Work on the CIF

The application domain of the CIF consists of languages and tools from computer science and from dynamics and control for modelling, simulation, analysis, controller synthesis, and verification in the area of untimed, timed and hybrid systems.

Example CIF model

The figure below shows a liquid storage tank with a volume controller VC. The incoming flow Qi can be controlled by means of a valve n. The outgoing flow is given by equation Qo = sqrt(V). The volume controller maintains the volume V of the liquid in the tank between 2 and 10.

CIF Tank Controller

The following is a specification of the controlled tank system in CIF 2:

model TankController()=
|[ cont control real V = 10.0
 ; var          real Qi, Qo
 ; disc control nat n = 0
:: Tank : |( mode physics = initial
                     inv V' = Qi - Qo
                       , Qi = n * 5.0
                       , Qo = sqrt(V)
          )|
||
   Controller : |( mode closed = initial
                                 (when V <= 2  now do n := 1) goto opened
                      , opened = (when V >= 10 now do n := 0) goto closed
                )|
]|

The following is a specification of the controlled tank system in CIF 1:

model TankController() =
|[ extern var V: cont real = 10
            ; Qi, Qo: alg real
            ; n: disc nat = 0
:: |( mode physics = inv dot V = Qi - Qo
                       &    Qi = n * 5
                       &    Qo = sqrt(V)
   :: physics
   )|
||
   |( mode closed = when V <= 2  now do n := 1 goto opened
         , opened = when V >= 10 now do n := 0 goto closed
   :: closed
   )|
]|

The CIF 1 simulator can be used to simulate both models and to produce the following figure:

Simulation results of CIF Tank Controller model

Further info on the CIF

Further info on CIF 2

Further info on CIF 1

cif/start.1421325059.txt.gz · Last modified: Thursday, 15 January 2015 : 13:30:59 by hvrooy