This is an old revision of the document!
For all new developments, please use the CIF 3 toolset, available via the CIF 3 website at http://cif.mn.wtb.tue.nl.
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.
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.
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.
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
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: