FUML15 — Defects in Base Semantics from fUML

There were found 42 issues, 5 of them were enhancements proposals, and 37 were defects.

The main issues concerning defects were:
1. The Base Semantics had a defect in the section 10.4.8.3 (pg. 383). There was missing a forall construction, which did not allow to parse entire definition.
2. After applied the necessary remedy actions to the definition, a model finder (EPROVER) was used to check if the fUML definition together with PSL definition - psl_outer_core - was satisfiable. The fUML Base Semantics together with PSL was unsatisfiable.
3. A model finder (EPROVER) also was used to check if the Base Semantics alone (without PSL) was satisfiable. The fUML Base Semantics was unsatisfiable.

I have been made available a file with all analyzed files at the following address:

http://es.cs.uni-kl.de/people/romero/fUMLOMGIssue20130630.zip

This file can help to recognize the defects.

Update subclause 10.4.8.3

Unfortunately, the file referenced in the issue is no longer available at the given link, and it was never physically attached to the issue (or, if it was at some point, it is now lost). Further, whether the base semantics are provably satisfiable has not seemed to be an issue in the successful use of fUML. Therefore, until someone takes the initiative to do further research and compile a new list of identified defects in the base semantics, it does not seem to be necessary to make any changes in this regard for now.

On the other hand, the defect specifically identified in subclause 10.4.8.3 is, indeed, an error that should be corrected.