XFG Language and its Profile for Modeling and Analysis of Energy-aware and real-timed behaviors

Eun-Young Kang*, Pierre-Yves Schobbens

*Corresponding author for this work

Research output: Book/anthology/thesis/reportReportResearch

Abstract

This report introduces a formal specification language XFG (extended function-block graphs), which can be used as IF (interchange format) for Timed Automata-based input modeling languages and model checkers. Section 1 informally represents a general introduction to XFG. The concrete E-BNF syntax rules are presented in Section 2. Section 3 defines complete syntax and semantics of the langauge. Section 4 gives a running example of the Brake-By-Wire (BBW) system and part of the XFG specification of the system. We propose a model-based approach to system engineering using XFG in Section 5. Section 6 defines a UML profile for XFG language based on EAST-ADL and MARTE. Finally, Section 7 provides model-to-text transformations to convert the profiled models into XFG language. 1 eXtended Function-block Graphs: XFG An XFG (eXtended Function-block Graphs) language is an extension of timed automata [2]. It is a formal specification interchange format language for modeling and analysis of energy-aware real-time (ERT) systems. The XFG format is a textual description language and it captures the axiomatic and operational specification of function aspects, and ERT behavior. The XFG language aims to establish interoperability of various tools by means of model transformations to and from XFG: The XFG is designed as an engineering language for formal specification and verification, serving as the Hybrid and Timed Automata (TA) [2, 1] based input modeling language for various model checkers such as UPPAAL series tool [6, 21], KRONOS [8, 7], and HYTECH [12, 11, 13], etc. An XFG system consisting of a number of graphes (processes) provides a simple representation for high-level specification languages and is suitable for modeling in-terprocess communication by value or signal passing though data channels. The basic building blocks for an XFG system are presented by processes and two basic constructions of the process in XFG are locations and edges. The process in XFG system represents a single thread of execution. Interprocess communication is represented by the synchronous edges. They communicate by means of shared variables or by synchronous value passing. The XFG process permits two-way synchronization communication (rendezvous-style) on complementary input and output actions, as well as broadcast actions. An edge labeled with a synchronization l!v with another labeled l?v or an arbitrary number of receivers l?v, where l is a synchronization channel name and v is a share variable.
Original languageEnglish
Number of pages36
Publication statusPublished - 2019

Fingerprint

Synchronization
Specification languages
Interchanges
Communication
Specifications
Real time systems
Systems engineering
Brakes
Interoperability
Semantics
Wire
Concretes
Formal specification
Modeling languages
Formal verification

Cite this

@book{952dba4c71764594a12dc49d68f0855e,
title = "XFG Language and its Profile for Modeling and Analysis of Energy-aware and real-timed behaviors",
abstract = "This report introduces a formal specification language XFG (extended function-block graphs), which can be used as IF (interchange format) for Timed Automata-based input modeling languages and model checkers. Section 1 informally represents a general introduction to XFG. The concrete E-BNF syntax rules are presented in Section 2. Section 3 defines complete syntax and semantics of the langauge. Section 4 gives a running example of the Brake-By-Wire (BBW) system and part of the XFG specification of the system. We propose a model-based approach to system engineering using XFG in Section 5. Section 6 defines a UML profile for XFG language based on EAST-ADL and MARTE. Finally, Section 7 provides model-to-text transformations to convert the profiled models into XFG language. 1 eXtended Function-block Graphs: XFG An XFG (eXtended Function-block Graphs) language is an extension of timed automata [2]. It is a formal specification interchange format language for modeling and analysis of energy-aware real-time (ERT) systems. The XFG format is a textual description language and it captures the axiomatic and operational specification of function aspects, and ERT behavior. The XFG language aims to establish interoperability of various tools by means of model transformations to and from XFG: The XFG is designed as an engineering language for formal specification and verification, serving as the Hybrid and Timed Automata (TA) [2, 1] based input modeling language for various model checkers such as UPPAAL series tool [6, 21], KRONOS [8, 7], and HYTECH [12, 11, 13], etc. An XFG system consisting of a number of graphes (processes) provides a simple representation for high-level specification languages and is suitable for modeling in-terprocess communication by value or signal passing though data channels. The basic building blocks for an XFG system are presented by processes and two basic constructions of the process in XFG are locations and edges. The process in XFG system represents a single thread of execution. Interprocess communication is represented by the synchronous edges. They communicate by means of shared variables or by synchronous value passing. The XFG process permits two-way synchronization communication (rendezvous-style) on complementary input and output actions, as well as broadcast actions. An edge labeled with a synchronization l!v with another labeled l?v or an arbitrary number of receivers l?v, where l is a synchronization channel name and v is a share variable.",
author = "Eun-Young Kang and Pierre-Yves Schobbens",
year = "2019",
language = "English",

}

XFG Language and its Profile for Modeling and Analysis of Energy-aware and real-timed behaviors. / Kang, Eun-Young; Schobbens, Pierre-Yves .

2019. 36 p.

Research output: Book/anthology/thesis/reportReportResearch

TY - RPRT

T1 - XFG Language and its Profile for Modeling and Analysis of Energy-aware and real-timed behaviors

AU - Kang, Eun-Young

AU - Schobbens, Pierre-Yves

PY - 2019

Y1 - 2019

N2 - This report introduces a formal specification language XFG (extended function-block graphs), which can be used as IF (interchange format) for Timed Automata-based input modeling languages and model checkers. Section 1 informally represents a general introduction to XFG. The concrete E-BNF syntax rules are presented in Section 2. Section 3 defines complete syntax and semantics of the langauge. Section 4 gives a running example of the Brake-By-Wire (BBW) system and part of the XFG specification of the system. We propose a model-based approach to system engineering using XFG in Section 5. Section 6 defines a UML profile for XFG language based on EAST-ADL and MARTE. Finally, Section 7 provides model-to-text transformations to convert the profiled models into XFG language. 1 eXtended Function-block Graphs: XFG An XFG (eXtended Function-block Graphs) language is an extension of timed automata [2]. It is a formal specification interchange format language for modeling and analysis of energy-aware real-time (ERT) systems. The XFG format is a textual description language and it captures the axiomatic and operational specification of function aspects, and ERT behavior. The XFG language aims to establish interoperability of various tools by means of model transformations to and from XFG: The XFG is designed as an engineering language for formal specification and verification, serving as the Hybrid and Timed Automata (TA) [2, 1] based input modeling language for various model checkers such as UPPAAL series tool [6, 21], KRONOS [8, 7], and HYTECH [12, 11, 13], etc. An XFG system consisting of a number of graphes (processes) provides a simple representation for high-level specification languages and is suitable for modeling in-terprocess communication by value or signal passing though data channels. The basic building blocks for an XFG system are presented by processes and two basic constructions of the process in XFG are locations and edges. The process in XFG system represents a single thread of execution. Interprocess communication is represented by the synchronous edges. They communicate by means of shared variables or by synchronous value passing. The XFG process permits two-way synchronization communication (rendezvous-style) on complementary input and output actions, as well as broadcast actions. An edge labeled with a synchronization l!v with another labeled l?v or an arbitrary number of receivers l?v, where l is a synchronization channel name and v is a share variable.

AB - This report introduces a formal specification language XFG (extended function-block graphs), which can be used as IF (interchange format) for Timed Automata-based input modeling languages and model checkers. Section 1 informally represents a general introduction to XFG. The concrete E-BNF syntax rules are presented in Section 2. Section 3 defines complete syntax and semantics of the langauge. Section 4 gives a running example of the Brake-By-Wire (BBW) system and part of the XFG specification of the system. We propose a model-based approach to system engineering using XFG in Section 5. Section 6 defines a UML profile for XFG language based on EAST-ADL and MARTE. Finally, Section 7 provides model-to-text transformations to convert the profiled models into XFG language. 1 eXtended Function-block Graphs: XFG An XFG (eXtended Function-block Graphs) language is an extension of timed automata [2]. It is a formal specification interchange format language for modeling and analysis of energy-aware real-time (ERT) systems. The XFG format is a textual description language and it captures the axiomatic and operational specification of function aspects, and ERT behavior. The XFG language aims to establish interoperability of various tools by means of model transformations to and from XFG: The XFG is designed as an engineering language for formal specification and verification, serving as the Hybrid and Timed Automata (TA) [2, 1] based input modeling language for various model checkers such as UPPAAL series tool [6, 21], KRONOS [8, 7], and HYTECH [12, 11, 13], etc. An XFG system consisting of a number of graphes (processes) provides a simple representation for high-level specification languages and is suitable for modeling in-terprocess communication by value or signal passing though data channels. The basic building blocks for an XFG system are presented by processes and two basic constructions of the process in XFG are locations and edges. The process in XFG system represents a single thread of execution. Interprocess communication is represented by the synchronous edges. They communicate by means of shared variables or by synchronous value passing. The XFG process permits two-way synchronization communication (rendezvous-style) on complementary input and output actions, as well as broadcast actions. An edge labeled with a synchronization l!v with another labeled l?v or an arbitrary number of receivers l?v, where l is a synchronization channel name and v is a share variable.

M3 - Report

BT - XFG Language and its Profile for Modeling and Analysis of Energy-aware and real-timed behaviors

ER -