A compositional interchange format for hybrid systems : design and implementation

D.E. Nadales Agut

Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)Academic

Abstract

The design of large industrial controlled systems is a difficult task, which calls for a modelbased design approach. For this, different formalisms exist. Each of these formalisms addresses a specific set of problems, and has its own set of features. Moreover, several formalisms and tools are used in each stage of the system development. As a consequence, there is a conspicuous need for integrated tool support for the design of large complex controlled systems, from the first concept to the implementation, and further on, over their entire life cycle. The Compositional Interchange Format (CIF) has been developed during this research to serve as an interchange format between different formalisms. CIF is an automata-based formalism, that allows to model and simulate hybrid systems. The language incorporates process algebraic operations, and has a formal semantics, based on the Structured Operational Semantics (SOS) framework. The semantics is shown to be compositional and we have proven that it preserves important algebraic properties, which express our intuition about the behavior of the language operators. CIF was extended with hierarchy (HCIF), to support the development of systems through stepwise refinement. The semantics of HCIF is given by means of SOS rules, and is defined in a compositional manner, by referring only to the transition system of the substructures, and not to their syntactic representation. This compositional introduction of hierarchy allows us to keep the semantics of the HCIF operators almost unchanged with respect to the CIF original semantics. A case-study on a patient support system is modeled in HCIF to show its applicability. Based on the formal description of CIF, we developed a simulator that conforms to the language semantics. We use the SOS specification of the language to obtain a new set of socalled symbolic rules. These rules contain the predicates that are required during simulation to compute time delays, and action updates. In this way, we present a rigorous method, which given the semantic specification of a complex language, allows us to obtain a simulator for models written in that language. We defined a linearization process for CIF terms, to allow the elimination of operators that are not natively supported in other languages, and to facilitate tool reuse. The linearization algorithm is obtained through a stepwise refinement of the original CIF SOS rules. As a result, we show how the semantic specification of the language can guide the implementation of such a procedure, yielding a simple proof of correctness. To enable the verification of timed CIF models, we formalized and proved a semanticpreserving transformation from CIF to Uppaal. Finally, the tools we developed were used in a complex case-study: the design of a controller for a miniature pipeless plant. In this way we show the applicability, as a proof of concept, of the toolchain developed in the FP7-MULTIFORM project. This toolchain involves controller synthesis, verification, and hybrid-systems simulation. In this thesis we show how formal semantics can be used not only for specifying mathematically a language, but also for developing tools and model transformations for it. However, working with such a degree of formalization requires the development of tool support for assisting this process. Otherwise the process is not maintainable nor scalable. In hindsight it is clear now that besides the mathematical correctness, the modeling convenience of a modeling formalism is crucial for its adoption. However in this thesis the effort was put mostly in the former aspect.
LanguageEnglish
QualificationDoctor of Philosophy
Awarding Institution
  • Department of Mechanical Engineering
Supervisors/Advisors
  • Rooda, Koos, Promotor
  • Baeten, Jos, Promotor
  • van Beek, Bert, Copromotor
Award date29 Nov 2012
Place of PublicationEindhoven
Publisher
Print ISBNs978-90-386-3249-0
DOIs
StatePublished - 2012

Fingerprint

Interchanges
Hybrid systems
Semantics
Systems analysis
Specifications
Linearization
Simulators
Controllers
Syntactics
Life cycle
Time delay

Cite this

Nadales Agut, D. E. (2012). A compositional interchange format for hybrid systems : design and implementation Eindhoven: Technische Universiteit Eindhoven DOI: 10.6100/IR737559
Nadales Agut, D.E.. / A compositional interchange format for hybrid systems : design and implementation. Eindhoven : Technische Universiteit Eindhoven, 2012. 225 p.
@phdthesis{28df6bb0e1694c1a8c6f86f2ee7833b0,
title = "A compositional interchange format for hybrid systems : design and implementation",
abstract = "The design of large industrial controlled systems is a difficult task, which calls for a modelbased design approach. For this, different formalisms exist. Each of these formalisms addresses a specific set of problems, and has its own set of features. Moreover, several formalisms and tools are used in each stage of the system development. As a consequence, there is a conspicuous need for integrated tool support for the design of large complex controlled systems, from the first concept to the implementation, and further on, over their entire life cycle. The Compositional Interchange Format (CIF) has been developed during this research to serve as an interchange format between different formalisms. CIF is an automata-based formalism, that allows to model and simulate hybrid systems. The language incorporates process algebraic operations, and has a formal semantics, based on the Structured Operational Semantics (SOS) framework. The semantics is shown to be compositional and we have proven that it preserves important algebraic properties, which express our intuition about the behavior of the language operators. CIF was extended with hierarchy (HCIF), to support the development of systems through stepwise refinement. The semantics of HCIF is given by means of SOS rules, and is defined in a compositional manner, by referring only to the transition system of the substructures, and not to their syntactic representation. This compositional introduction of hierarchy allows us to keep the semantics of the HCIF operators almost unchanged with respect to the CIF original semantics. A case-study on a patient support system is modeled in HCIF to show its applicability. Based on the formal description of CIF, we developed a simulator that conforms to the language semantics. We use the SOS specification of the language to obtain a new set of socalled symbolic rules. These rules contain the predicates that are required during simulation to compute time delays, and action updates. In this way, we present a rigorous method, which given the semantic specification of a complex language, allows us to obtain a simulator for models written in that language. We defined a linearization process for CIF terms, to allow the elimination of operators that are not natively supported in other languages, and to facilitate tool reuse. The linearization algorithm is obtained through a stepwise refinement of the original CIF SOS rules. As a result, we show how the semantic specification of the language can guide the implementation of such a procedure, yielding a simple proof of correctness. To enable the verification of timed CIF models, we formalized and proved a semanticpreserving transformation from CIF to Uppaal. Finally, the tools we developed were used in a complex case-study: the design of a controller for a miniature pipeless plant. In this way we show the applicability, as a proof of concept, of the toolchain developed in the FP7-MULTIFORM project. This toolchain involves controller synthesis, verification, and hybrid-systems simulation. In this thesis we show how formal semantics can be used not only for specifying mathematically a language, but also for developing tools and model transformations for it. However, working with such a degree of formalization requires the development of tool support for assisting this process. Otherwise the process is not maintainable nor scalable. In hindsight it is clear now that besides the mathematical correctness, the modeling convenience of a modeling formalism is crucial for its adoption. However in this thesis the effort was put mostly in the former aspect.",
author = "{Nadales Agut}, D.E.",
year = "2012",
doi = "10.6100/IR737559",
language = "English",
isbn = "978-90-386-3249-0",
publisher = "Technische Universiteit Eindhoven",
school = "Department of Mechanical Engineering",

}

Nadales Agut, DE 2012, 'A compositional interchange format for hybrid systems : design and implementation', Doctor of Philosophy, Department of Mechanical Engineering, Eindhoven. DOI: 10.6100/IR737559

A compositional interchange format for hybrid systems : design and implementation. / Nadales Agut, D.E.

Eindhoven : Technische Universiteit Eindhoven, 2012. 225 p.

Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)Academic

TY - THES

T1 - A compositional interchange format for hybrid systems : design and implementation

AU - Nadales Agut,D.E.

PY - 2012

Y1 - 2012

N2 - The design of large industrial controlled systems is a difficult task, which calls for a modelbased design approach. For this, different formalisms exist. Each of these formalisms addresses a specific set of problems, and has its own set of features. Moreover, several formalisms and tools are used in each stage of the system development. As a consequence, there is a conspicuous need for integrated tool support for the design of large complex controlled systems, from the first concept to the implementation, and further on, over their entire life cycle. The Compositional Interchange Format (CIF) has been developed during this research to serve as an interchange format between different formalisms. CIF is an automata-based formalism, that allows to model and simulate hybrid systems. The language incorporates process algebraic operations, and has a formal semantics, based on the Structured Operational Semantics (SOS) framework. The semantics is shown to be compositional and we have proven that it preserves important algebraic properties, which express our intuition about the behavior of the language operators. CIF was extended with hierarchy (HCIF), to support the development of systems through stepwise refinement. The semantics of HCIF is given by means of SOS rules, and is defined in a compositional manner, by referring only to the transition system of the substructures, and not to their syntactic representation. This compositional introduction of hierarchy allows us to keep the semantics of the HCIF operators almost unchanged with respect to the CIF original semantics. A case-study on a patient support system is modeled in HCIF to show its applicability. Based on the formal description of CIF, we developed a simulator that conforms to the language semantics. We use the SOS specification of the language to obtain a new set of socalled symbolic rules. These rules contain the predicates that are required during simulation to compute time delays, and action updates. In this way, we present a rigorous method, which given the semantic specification of a complex language, allows us to obtain a simulator for models written in that language. We defined a linearization process for CIF terms, to allow the elimination of operators that are not natively supported in other languages, and to facilitate tool reuse. The linearization algorithm is obtained through a stepwise refinement of the original CIF SOS rules. As a result, we show how the semantic specification of the language can guide the implementation of such a procedure, yielding a simple proof of correctness. To enable the verification of timed CIF models, we formalized and proved a semanticpreserving transformation from CIF to Uppaal. Finally, the tools we developed were used in a complex case-study: the design of a controller for a miniature pipeless plant. In this way we show the applicability, as a proof of concept, of the toolchain developed in the FP7-MULTIFORM project. This toolchain involves controller synthesis, verification, and hybrid-systems simulation. In this thesis we show how formal semantics can be used not only for specifying mathematically a language, but also for developing tools and model transformations for it. However, working with such a degree of formalization requires the development of tool support for assisting this process. Otherwise the process is not maintainable nor scalable. In hindsight it is clear now that besides the mathematical correctness, the modeling convenience of a modeling formalism is crucial for its adoption. However in this thesis the effort was put mostly in the former aspect.

AB - The design of large industrial controlled systems is a difficult task, which calls for a modelbased design approach. For this, different formalisms exist. Each of these formalisms addresses a specific set of problems, and has its own set of features. Moreover, several formalisms and tools are used in each stage of the system development. As a consequence, there is a conspicuous need for integrated tool support for the design of large complex controlled systems, from the first concept to the implementation, and further on, over their entire life cycle. The Compositional Interchange Format (CIF) has been developed during this research to serve as an interchange format between different formalisms. CIF is an automata-based formalism, that allows to model and simulate hybrid systems. The language incorporates process algebraic operations, and has a formal semantics, based on the Structured Operational Semantics (SOS) framework. The semantics is shown to be compositional and we have proven that it preserves important algebraic properties, which express our intuition about the behavior of the language operators. CIF was extended with hierarchy (HCIF), to support the development of systems through stepwise refinement. The semantics of HCIF is given by means of SOS rules, and is defined in a compositional manner, by referring only to the transition system of the substructures, and not to their syntactic representation. This compositional introduction of hierarchy allows us to keep the semantics of the HCIF operators almost unchanged with respect to the CIF original semantics. A case-study on a patient support system is modeled in HCIF to show its applicability. Based on the formal description of CIF, we developed a simulator that conforms to the language semantics. We use the SOS specification of the language to obtain a new set of socalled symbolic rules. These rules contain the predicates that are required during simulation to compute time delays, and action updates. In this way, we present a rigorous method, which given the semantic specification of a complex language, allows us to obtain a simulator for models written in that language. We defined a linearization process for CIF terms, to allow the elimination of operators that are not natively supported in other languages, and to facilitate tool reuse. The linearization algorithm is obtained through a stepwise refinement of the original CIF SOS rules. As a result, we show how the semantic specification of the language can guide the implementation of such a procedure, yielding a simple proof of correctness. To enable the verification of timed CIF models, we formalized and proved a semanticpreserving transformation from CIF to Uppaal. Finally, the tools we developed were used in a complex case-study: the design of a controller for a miniature pipeless plant. In this way we show the applicability, as a proof of concept, of the toolchain developed in the FP7-MULTIFORM project. This toolchain involves controller synthesis, verification, and hybrid-systems simulation. In this thesis we show how formal semantics can be used not only for specifying mathematically a language, but also for developing tools and model transformations for it. However, working with such a degree of formalization requires the development of tool support for assisting this process. Otherwise the process is not maintainable nor scalable. In hindsight it is clear now that besides the mathematical correctness, the modeling convenience of a modeling formalism is crucial for its adoption. However in this thesis the effort was put mostly in the former aspect.

U2 - 10.6100/IR737559

DO - 10.6100/IR737559

M3 - Phd Thesis 1 (Research TU/e / Graduation TU/e)

SN - 978-90-386-3249-0

PB - Technische Universiteit Eindhoven

CY - Eindhoven

ER -

Nadales Agut DE. A compositional interchange format for hybrid systems : design and implementation. Eindhoven: Technische Universiteit Eindhoven, 2012. 225 p. Available from, DOI: 10.6100/IR737559