search

INTO-CPS-Association / fmi_utilities

1 stars 0 forks source link

FMIChecker text #9

Closed CThuleHansen closed 4 years ago

CThuleHansen commented 4 years ago

I would like some text presenting the FMI Checker at https://sweng.au.dk/fmiutils/fmichecker.

I will propose some text, and then I hope that you @nickbattle will go over it :)

I will take care of putting it on the website once we have some text that we agree to.

CThuleHansen commented 4 years ago

Proposed text:

The FMI specification is semi-formal and allows for different interpretations, which lead to different implementations of FMUs. The FMI Checker is an attempt to formalise the static constraints of the FMI standard - the model description file and provide checking facilities.

The formalisation is carried out in VDM-SL and the VDM-SL specification is used to check the uploaded model description file. The source code of the FMI Checker is available at: https://github.com/INTO-CPS-Association/FMI-VDM-Model

If you disagree with a checking result then we are very interested in hearing about it!
It will allow us to pin down a more accurate interpretation of the standard, and (possibly) correct issues in the tools. Please report issues here: https://github.com/INTO-CPS-Association/FMI-VDM-Model/issues

This approach is also presented in the article TODO: REF PUBLICATION

nickbattle commented 4 years ago

Thanks Casper, that's pretty close. Are we intending to call it the "FMI Checker" or "VDMCheck"? Or is the idea that the "FMI Checker" is an online resource that incorporates a suite of tools? Some suggested tweaks to the wording below: ...

The FMI specification is semi-formal. This can lead to different interpretations, which can in turn lead to different FMU implementations. The FMI Checker is an attempt to formalise the static constraints of the FMI standard - the model description file - and provide a tool to automatically check an FMU.

The formalisation is defined as a VDM-SL specification, which is used to check the uploaded model description file. The VDM model and source code of the FMI Checker is available at: https://github.com/INTO-CPS-Association/FMI-VDM-Model.

If you disagree with a checking result then we are very interested to hear about it! This will allow us to pin down a more accurate interpretation of the standard, and (possibly) correct issues in the tools. Please report issues here: https://github.com/INTO-CPS-Association/FMI-VDM-Model/issues.

CThuleHansen commented 4 years ago

I have not really given much thought to the name. Maybe it should be FMIStaticChecker? Something that conveys its meaning on the website?

As I said, I have not really thought very much about this. Just sort of went with a name :)

nickbattle commented 4 years ago

If we intend to include the "mobster" as well as VDMCheck in the same site (and that would be fine by me!), and possibly even more dynamic checks in future, a generic name like "FMI Checker" would seem ok. Is it an FMI checker or FMU checker? :-)

CThuleHansen commented 4 years ago

Mobster is currently under fmu analyzer. So we have fmi checker and fmu analyzer. Maybe it shoudl be fmu static checker and fmu dynamic checker? @clagms you are invited to the discussion :)

nickbattle commented 4 years ago

As yes, I see. Yes, calling them static and dynamic would be fine by me, though are users generally clear about the difference? I guess so: one just looks at the "dead" FMU config, the other tries to run it...

CThuleHansen commented 4 years ago

That is where the proposed text comes in :) Since the page is called FMI Utilities I propose: Static Checker and Dynamic Checker @clagms what do you think? @nickbattle OK?

clagms commented 4 years ago

Maybe it shoudl be fmu static checker and fmu dynamic checker

I think this is better indeed, provided that we explain what we mean by static and dynamic. Something like:

FMI Static Check focuses on the metadata provided by the FMU (e.g., the model description file). It will not generally ask the FMU to compute stuff. For example, while the binaries may be loaded, it will not call functions such as getReal and setReal, or *doStep. FMI Dynamic Check focuses on the behavior of the FMU. It will load the binaries, invoke any FMU function, and will observe the results computed by the FMU.

@nickbattle please correct because I'm not up to date with what the FMI Static checker is doing. If the FMI Static check is asking the FMU to compute stuff (e.g., calling getReal functions), then I think the best would be unify everything under the same name, and just call it FMI Checker (then the user has a single fron-end, and he gets different the static and dynamic results, and in the future he will get a more unified report).

Regarding the FMIMOBSTER name, while I'm very fond of it, it is actually describing how we do the dynamic checks (through model based testing). In the future, this approach may change, so having a more generic name that describes the goal (Dynamic Check) and not the approach is better.

nickbattle commented 4 years ago

Hi Claudio. The static checker only looks at the XML file - ie. the VDM model is not concerned with the FMU binaries and does not attempt to call any functions. The VDM dynamic model doesn't call any functions either(!) - it is a model of what an FMU can do given its static configuration, rather than a way to exercise a real FMU (eg. if you call getReal for a variable that doesn't exist, you will get a well defined error).

CThuleHansen commented 4 years ago

Static and dynamic it is!