Syntax and semantics of the compositional interchange format for hybrid systems

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

Research output: Contribution to journalArticleAcademicpeer-review

12 Citations (Scopus)

Abstract

Different modeling formalisms for timed and hybrid systems exist, each of which addresses a specific set of problems, and has its own set of features. These formalisms and tools can be used in each stage of the embedded systems development, to verify and validate various requirements. The Compositional Interchange Format (CIF), is a formalism based on hybrid automata, which are composed using process algebraic operators. CIF aims to establish interoperability among a wide range of formalisms and tools by means of model transformations and co-simulation, which avoids the need for implementing many bilateral translators. This work presents the syntax and formal semantics of CIF. The semantics is shown to be compositional, and proven to preserve certain algebraic properties, which express our intuition about the behavior of the language operators. In addition we show how CIF operators can be combined to implement widely used constructs present in other timed and hybrid formalisms, and we illustrate the applicability of the formalism by developing several examples. Based on the formal specification of CIF, an Eclipse based simulation environment has been developed. We expect this work to serve as the basis for the formal definition of semantic preserving transformations between various languages for the specification of timed and hybrid systems.
LanguageEnglish
Pages1-52
Number of pages52
JournalJournal of Logic and Algebraic Programming
Volume82
Issue number1
DOIs
StatePublished - 2013

Fingerprint

Interchanges
Hybrid systems
Hybrid Systems
Semantics
Operator
Hybrid Automata
Co-simulation
Formal Semantics
Formal Specification
Model Transformation
System Development
Simulation Environment
Embedded Systems
Interoperability
Express
Specification
Verify
Embedded systems
Requirements
Modeling

Cite this

@article{fb05b683b9664c66baa1b9ae636335a1,
title = "Syntax and semantics of the compositional interchange format for hybrid systems",
abstract = "Different modeling formalisms for timed and hybrid systems exist, each of which addresses a specific set of problems, and has its own set of features. These formalisms and tools can be used in each stage of the embedded systems development, to verify and validate various requirements. The Compositional Interchange Format (CIF), is a formalism based on hybrid automata, which are composed using process algebraic operators. CIF aims to establish interoperability among a wide range of formalisms and tools by means of model transformations and co-simulation, which avoids the need for implementing many bilateral translators. This work presents the syntax and formal semantics of CIF. The semantics is shown to be compositional, and proven to preserve certain algebraic properties, which express our intuition about the behavior of the language operators. In addition we show how CIF operators can be combined to implement widely used constructs present in other timed and hybrid formalisms, and we illustrate the applicability of the formalism by developing several examples. Based on the formal specification of CIF, an Eclipse based simulation environment has been developed. We expect this work to serve as the basis for the formal definition of semantic preserving transformations between various languages for the specification of timed and hybrid systems.",
author = "{Nadales Agut}, D.E. and {Beek, van}, D.A. and J.E. Rooda",
year = "2013",
doi = "10.1016/j.jlap.2012.07.001",
language = "English",
volume = "82",
pages = "1--52",
journal = "Journal of Logic and Algebraic Programming",
issn = "1567-8326",
publisher = "Elsevier",
number = "1",

}

Syntax and semantics of the compositional interchange format for hybrid systems. / Nadales Agut, D.E.; Beek, van, D.A.; Rooda, J.E.

In: Journal of Logic and Algebraic Programming, Vol. 82, No. 1, 2013, p. 1-52.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Syntax and semantics of the compositional interchange format for hybrid systems

AU - Nadales Agut,D.E.

AU - Beek, van,D.A.

AU - Rooda,J.E.

PY - 2013

Y1 - 2013

N2 - Different modeling formalisms for timed and hybrid systems exist, each of which addresses a specific set of problems, and has its own set of features. These formalisms and tools can be used in each stage of the embedded systems development, to verify and validate various requirements. The Compositional Interchange Format (CIF), is a formalism based on hybrid automata, which are composed using process algebraic operators. CIF aims to establish interoperability among a wide range of formalisms and tools by means of model transformations and co-simulation, which avoids the need for implementing many bilateral translators. This work presents the syntax and formal semantics of CIF. The semantics is shown to be compositional, and proven to preserve certain algebraic properties, which express our intuition about the behavior of the language operators. In addition we show how CIF operators can be combined to implement widely used constructs present in other timed and hybrid formalisms, and we illustrate the applicability of the formalism by developing several examples. Based on the formal specification of CIF, an Eclipse based simulation environment has been developed. We expect this work to serve as the basis for the formal definition of semantic preserving transformations between various languages for the specification of timed and hybrid systems.

AB - Different modeling formalisms for timed and hybrid systems exist, each of which addresses a specific set of problems, and has its own set of features. These formalisms and tools can be used in each stage of the embedded systems development, to verify and validate various requirements. The Compositional Interchange Format (CIF), is a formalism based on hybrid automata, which are composed using process algebraic operators. CIF aims to establish interoperability among a wide range of formalisms and tools by means of model transformations and co-simulation, which avoids the need for implementing many bilateral translators. This work presents the syntax and formal semantics of CIF. The semantics is shown to be compositional, and proven to preserve certain algebraic properties, which express our intuition about the behavior of the language operators. In addition we show how CIF operators can be combined to implement widely used constructs present in other timed and hybrid formalisms, and we illustrate the applicability of the formalism by developing several examples. Based on the formal specification of CIF, an Eclipse based simulation environment has been developed. We expect this work to serve as the basis for the formal definition of semantic preserving transformations between various languages for the specification of timed and hybrid systems.

U2 - 10.1016/j.jlap.2012.07.001

DO - 10.1016/j.jlap.2012.07.001

M3 - Article

VL - 82

SP - 1

EP - 52

JO - Journal of Logic and Algebraic Programming

T2 - Journal of Logic and Algebraic Programming

JF - Journal of Logic and Algebraic Programming

SN - 1567-8326

IS - 1

ER -