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 . 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.
|Number of pages||36|
|Publication status||Published - 2019|