Se.wtb.tue.nl

Compositional Interchange Format for HybridSystems (CIF The main purpose of the Compositional Interchange Format (CIF)[1], that hasoriginally been developed in HYCON, see [2] and [3, 4, 5, 6], is to establishinter-operability of a wide range of tools by means of model transformations toand from the CIF. In addition, the CIF provides a generic modeling formalismand tools for a wide range of untimed, timed and hybrid systems. An overviewon previous related work on interchange formalisms, such as found in [7], [8],[9], can be found in [3, 4].
The concepts in the CIF and the relations between them are defined in a so-called conceptual or meta model, see [1]. This model is defined in terms of(Ecore) class diagrams [10]. From these class diagrams, XML Schema definitions(XSDs) [11] have been generated. The XML Schema definitions as well as theEcore models can be obtained electronically via [12].
Regarding concrete syntax and behavioral semantics, the CIF consists of an abstract format, which is specified using a mathematical notation and is usedfor the definition of the formal semantics, and a concrete format, as definedin [5], which is specified in the ASCII character set by a formal grammar andis used as a modeling language. The operational semantics of a model in theabstract format is defined formally in a SOS style [13]. It defines the math-ematical meaning of a hybrid model in terms of an hybrid transition system.
The semantics of a model in the concrete format is formally defined by meansof a mapping to the abstract format. The advantage of having two formats isthat each can be tailored to its specific purpose. In general, the abstract formathas fewer concepts in order to simplify the semantics, while the concrete formathas ‘syntactic sugar’ and more emphasis on backward compatibility in order tofacilitate modeling. In [14], the concepts of the (concrete) CIF are illustratedby means of a hybrid model of a supermarket refrigeration system that exhibitsboth, nonlinear DAE dynamics as well as significant discrete dynamics, andserves as a challenging case study for hybrid control techniques in several Euro-pean research projects. More information about CIF and CIF tools allowing, e.g., simulation and visualization, can be found in [12].
The CIF serves as the basis of the European research project MULTIFORM,see [15]. The main objective of this project is to develop interoperability oftools and methods based on different modeling formalisms to provide integratedcoherent tool support for the design of large complex controlled systems. WithinMULTIFORM, algorithms and tools for the translation to/from the CIF willbe defined for a large variety of modeling languages, including Chi, gPROMS,Matlab/Simulink, Modelica, MUSCOD-II, PHAVer, and UPPAAL.
Depending on the availability of a formal definition of the behavioral se- mantics of a language, two different categories of transformations can be distin-guished: • Transformations from formalisms that have formal semantics to the CIF (vice • Translations from formalisms that do not have formal semantics to the Transformations between formalisms with formal se-mantics In case of a translation where the source formalism as well as the target for-malisms have formal semantics, one can define an equivalence relation 1 betweenthe semantics of the two formalisms. By means of mathematical proof, it canbe shown that the behavior of an input model and the behavior of the outputmodel of the translation are equivalent.
To illustrate this approach, consider the translation of hybrid automata [16] to the CIF. The semantics of a hybrid automaton is a timed transition sys-tem with two types of transitions: action transitions (corresponding to controlswitches) and time transitions (corresponding to continuous behavior in a con-trol mode). On the other hand, the semantics of a CIF automaton is a hybridtransition system which also has these two types of transitions. The main differ-ence between these semantics is in the labeling of the action and time transitions.
In timed transition systems the labels of action transitions are simply the eventsof the hybrid automaton, whereas the labels of the action transitions of a hybridtransition system also contain the valuations of the model variables prior to andafter the action. For time transitions, the labels in a timed transition systemcontain only the duration of the time transition whereas time transitions in hy-brid transition systems also have the trajectory of the model variables as a label.
Finally, a timed transition system can have many initial states whereas a hybrid 1In fact multiple equivalence relations can be defined depending on the properties to be transition system has only one initial state. This one initial state captures thebehavior of all the initial states of the timed transition system.
Let ¯h be a mapping that maps a hybrid transition system onto a timed transition system by removing valuations from action transitions and trajecto-ries from time transitions. Furthermore, let HA be a hybrid automaton and letMCIF be the CIF specification associated to it by its translation. Furthermore, let TTS and HTS be the semantics of HA and MCIF, respectively.
Then, there exists a (strong-)bisimulation relation [17, 18], denoted by ↔ , between the states of TTS and the states of ¯ from an initial state of TTS can be simulated by the initial state of ¯ and each transition from the initial state of ¯ Examples of similar translations including their correctness proofs can be found in [19, 20] (Translation of χ to 1) piecewise affine systems and 2) hybridautomata), and [21, 22] (Translation of χ to UPPAAL).
Transformations between formalisms with formal se-mantics In case of a translation where the source formalism does not have a formal se-mantics and the target formalism has a formal semantics, then, by means of a(formally defined) translation, formal semantics is given to the source formal-ism. An example of this approach can be found in [23] that defines bidirectionaltransformations between gPROMS and Modelica via the CIF. The correct-ness of the translations has been validated by means of comparing the simulationresults of several input models and their respective output models.
[1] D.E. Nadales Agut, D.A. van Beek, R.R.H. Schiffelers, D. Hendriks, and J.E. Rooda. Revision and extension of the CIF including data types andtransfer format. Technical Report D 1.1.1, MULTIFORM, 2009.
[2] HYCON Network of Excellence. http://www.ist-hycon.org/, 2005.
[3] D. A. van Beek, M. A. Reniers, R. R. H. Schiffelers, and J. E. Rooda. Foun- dations of an interchange format for hybrid systems. In Alberto Bemporad,Antonio Bicchi, and Giorgio Butazzo, editors, Hybrid Systems: Computa-tion and Control, 10th International Workshop, volume 4416 of LectureNotes in Computer Science, pages 587–600, Pisa, 2007. Springer-Verlag.
[4] D. A. van Beek, M. A. Reniers, J. E. Rooda, and R. R. H. Schiffelers.
Revised hybrid system interchange format. Technical Report HYCON De-liverable D3.6.3, HYCON NoE, 2007.
[5] D. A. van Beek, M. A. Reniers, J. E. Rooda, and R. R. H. Schiffelers.
Concrete syntax and semantics of the compositional interchange formatfor hybrid systems. In 17th Triennial World Congress of the InternationalFederation of Automatic Control, pages 7979–7986, Seoul, Korea, 2008.
[6] D. A. van Beek, P. Collins, D. E. Nadales, J.E. Rooda, and R. R. H.
Schiffelers. New concepts in the abstract format of the compositional inter-change format. In A. Giua, C. Mahuela, M. Silva, and J. Zaytoon, editors,3rd IFAC Conference on Analysis and Design of Hybrid Systems, pages250–255, Zaragoza, Spain, 2009.
[7] MoBIES team. HSIF semantics. Technical report, University of Pennsyl- [8] Alessandro Pinto, Luca P. Carloni, Roberto Passerone, and Alberto L.
Sangiovanni-Vincentelli. Interchange format for hybrid systems: Abstractsemantics. In Jo˜ ao P. Hespanha and Ashish Tiwari, editors, Hybrid Sys- tems: Computation and Control, 9th International Workshop, volume 3927of Lecture Notes in Computer Science, pages 491–506, Santa Barbara, 2006.
Springer-Verlag.
[9] Stefano Di Cairano, Alberto Bemporad, and Michal Kvasnica. An archi- tecture for data interchange of switched linear systems. Technical ReportD 3.3.1, HYCON NoE, 2006.
[10] Dave Steinberg, Frank Budinsky, Marcelo Paternostro, and Ed Merks. EMF Eclipse Modeling Framework. Addison-Wesley, 2009.
http://www.w3.org/TR/xmlschema-1/, 2004.
http://se.wtb.tue.nl/sewiki/cif, 2008.
[13] Gordon D. Plotkin. A structural approach to operational semantics. Jour- nal of Logic and Algebraic Programming, 60-61:17–139, 2004.
[14] C. Sonntag, R. R. H. Schiffelers, D. A. van Beek, J. E. Rooda, and S. Engell.
Modeling and simulation using the Compositional Interchange Format forhybrid systems. In I. Troch and F. Breitenecker, editors, 6th InternationalConference on Mathematical Modelling, Vienna, Austria, 2009.
for the design of networked embedded control systems MULTIFORM.
http://www.multiform.bci.tu-dortmund.de, 2008.
[16] T. A. Henzinger. The theory of hybrid automata. In M. K. Inan and R. P.
Kurshan, editors, Verification of Digital and Hybrid Systems, volume 170of NATO ASI Series F: Computer and Systems Science, pages 265–292.
Springer-Verlag, New York, 2000.
[17] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
[18] D. M. R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings 5th GI Conference, volume 104 of LectureNotes in Computer Science, pages 167–183. Springer-Verlag, 1981.
[19] K. L. Man and R. R. H. Schiffelers. Formal Specification and Analysis of Hybrid Systems. PhD thesis, Eindhoven University of Technology, 2006.
[20] D. A. van Beek, J. E. Rooda, R. R. H. Schiffelers, K. L. Man, and M. A.
Reniers. Relating hybrid Chi to other formalisms. Electronic Notes inTheoretical Computer Science, 191:85–113, 2007.
[21] E. M. Bortnik, D. A. van Beek, J. M. van de Mortel-Fronczak, and J. E.
Rooda. Verification of timed Chi models using Uppaal. In J. Filipe, J. A.
Cetto, and J.-L. Ferrier, editors, ICINCO 2005, Second International Con-ference on Informatics in Control, Automation and Robotics, pages 486–492, Barcelona, 2005. INSTICC Press.
[22] E. M. Bortnik. Formal methods in support of SMC design. PhD thesis, Eindhoven University of Technology, 2008.
[23] Christian Sonntag, Martin Hfner, and Adalat Jabrayilov. Realization of the model exchange with Modelica and gPROMS. Technical Report D 1.4.1,MULTIFORM, 2009.

Source: http://se.wtb.tue.nl/sewiki/_media/cif/ciftranslations.pdf