A Formal Treatment of FMI Sample Clauses

A Formal Treatment of FMI. ‌ To highlight and uncover issues with the evolving FMI standard, and to investigate the FMI formally, Xxxxxx et al [BBG+13] develop FMI’s most influential formalisation to date. This formalisation of a relevant subset of the FMI standard consists of a state-based functional model; relevant procedures of FMI’s API (abstract programming interface), which acts as the interface between MA and the slave FMUs, are modelled as functions. The paper studies FMI’s main subject-matter: simulations of continuous models based on numerical methods to approximate differential equations. Desirable properties of such methods are convergence (whether the method approximates the solution) and stability (whether errors are damped out). To ensure convergence, [BBG+13] investigates determinism, studying the situations under which determinate execution is ensured — that is, different runs of a MA on a given FMU network give the same results. To avoid nondeterminism and the possibility of unexpected results, the paper proposes a way to check for the absence of algebraic loops (convergence cannot be guaranteed in the presence of algebraic loops) by checking the acyclicity of the directed graph describing the dependencies between input and output ports of FMUs. The MAs of [BBG+13] preclude configurations with algebraic loops and are proved to be determinate. Although the model is formal, the proofs of the paper’s main theorems are rigorous and grounded on the paper’s formalisation, but they are not formal. It is interesting to comment on the emphasis that [BBG+13] puts on deter- minism. In a hybrid co-simulation setting made up of continuous and discrete components, nondeterminism may not necessarily be a bad thing. Continu- ous models may have non-determinism when they have components that rely on random numbers, for instance. Abstract models of discrete systems are often nondeterministic; that is seen as a means to achieve abstraction [HJ89]. Although nondeterminism is often at odds with model executability [HJ89], the discrete modelling community has found ways of conciliating these two opposing forces. The formal model of [BBG+13] would have to be refactored to be applicable to a world of possibly non-deterministic discrete components as all the API procedures are modelled as total functions. Given that the authors of [BBG+13] observe in [BGL+14] that the FMI should be appli- cable to general-purpose hybrid systems, it appears that the emphasis on determinacy should be relaxed...