This presentation focus on advances on Model Based System Engineering that fUML [1] brings. fUML, better known has Executable UML, provide a formalization of a subset of UML. UML, and with some extensions and adaptations SysML, can now be analysed in a formal way. That was main grief made by researchers.
First part of the presentation illustrates what is now possible by picking ideas from existing tools, notably Alloy [1] and OWL [3]. Following this path will enlighten what still must be done from researchers. It also points out how UML/SysML editors and tools can be enhanced. Indeed in current tools you can modelize activities that are not executable, you can describe Class/Block that cannot be instantiated, and so on.
The second part is about current implementation of previous ideas. It starts with a panorama of tools that can be combined, reused or adapted for the new desired features. For instance, it is possible to generate random instances of a model. Doing so helps to be confident in the model constraints. Moreover details will be given on how Topcased ease or not the integration of such a tool in its suite. For instance, it will be shown how Acceleo and ATL are used, but further details will also be given on how it integrates deeply with Topcased Editors for warnings, quick-fixes and so on.
2. Real models are complex.
Syntactical verifications are
nice but not enough.
More model semantics
checking is needed.
4th february 2011 Loïc Fejoz 2/19
3. Ok those are simple examples
but you can imagine others...
4th february 2011 Loïc Fejoz 3/19
4. This one could be very tricky
as the Generalization is not
drawn on the diagram.
4th february 2011 Loïc Fejoz 4/19
5. Activities verification
is the #1 priority of
the group that has
written the report
called "Executable
UML/SysML
semantics project
report"
4th february 2011 Loïc Fejoz 5/19
6. Your models certainly
contain less obvious
examples
(especially for cross-diagram
elements)
Remember that not all
elements are visible on
diagram. Moreover they are
cross-cutting concerns of
diagrams.
4th february 2011 Loïc Fejoz 6/19
8. FUML does not axiomatize all
UML. It does not axiomatize
SysML, nor OCL. But it can be
trivialy extended for those
examples.
Those formulae are written in
Common Logic Format (CLIF) with
Process Specification Language
(PSL).
(buml:Classifier “ZooPackage::SelfContentBlock“)
(buml:Property “ZooPackage::SelfContentBlock::subpart“)
(buml:ownedAttribute
“ZooPackage::SelfContentBlock“
“ZooPackage::SelfContentBlock::subpart“)
(buml:aggregation “ZooPackage::SelfContentBlock::subpart“ buml:composite)
…
(forall (o v f)
(if (and
(form:classifies “ZooPackage::SelfContentBlock“ o f)
(form:property-value o “ZooPackage::SelfContentBlock::subpart“ v f))
(= o v)))
4th february 2011 Loïc Fejoz 8/19
9. fULM Axiomatization
Boolean primitive types axiomatization:
(forall (x)
(if (buml:Boolean x) Obviously fUML provides
(or (= x form:true) axiomatization for primitive
(= x form:false)))) types, Classification, activity,
etc.
(not (= form:true form:false))
…
Classification and generalization:
(forall (csub csuper o f)
(iff (buml:general csub csuper)
(if (form:classifies csub o f)
(form:classifies csuper o f))))
4th february 2011 Loïc Fejoz 9/19
10. Those formulae may be verified
automatically by some provers.
Thus models can be formally
verified
(and shall be).
4th february 2011 Loïc Fejoz 10/19
11. Following slides will list tools
and difficulty we have to
develop an fUML plugin for
Topcased.
Time for a plugin !
4th february 2011 Loïc Fejoz 11/19
12. Acceleo MTL
The generated Java is nor
easy to (unit)test nor easy to
call. To few documentations for
programmatic use.
[template class2clif(clz : Class)]
(buml:Classifier [clz.clifName()/])
[for (gen : Generalization | clz.generalization)]
(buml:general [gen.specific.clifName()/]
[gen.general.clifName()/])
[/for]
[for (prop : Property | clz.ownedAttribute)]
[property2clif(prop, clz)/]
[/for]
[/template]
4th february 2011 Loïc Fejoz 12/19
13. We would prefer to use QVT
but the ATL implementation is
more advance.
Not easy to write unit-tests
especially when comparing
with QVT.
Usually we run ATL then MTL
but it is not that easy to chain
both tool without creating
ATL intermediate files.
vs
QVT
4th february 2011 Loïc Fejoz 13/19
14. This are getting better and
easier from version to version.
No documentation (again!) but
the code of the simple
verification made by TopCased
editor is easy to read and
reproduce.
Warnings and errors
as feedbacks
4th february 2011 Loïc Fejoz 14/19
15. If we generate warnings it
would be nice to propose
quickfixes. We were not able to
program some! There are stuff
missing to do that... Moreover
there are no documentation
nor existing code.
Quickfix?
Which quickfix?
4th february 2011 Loïc Fejoz 15/19
16. A little bit of topic but... At one point we tried to extends the SysML
activity diagram editor so as to present (some)
activities with a different looking.
We manage to do it but we violate some
access restriction. The code is not written for
that purpose and reuse is not made easy. Lots
of copy'n paste.
No documentation nor existing code.
Diagram extension
4th february 2011 Loïc Fejoz 16/19
17. As we generate files for external programs, we
have build a special builder to generate files on
model modification but we also tried to update
the model from files content.
It is a real nightmare...
ResourceSet,
Builder
and
model updates
4th february 2011 Loïc Fejoz 17/19
18. Topcased evolves quite quickly so bugs are quickly
corrected. BUT plugins also change to quickly and
sometime (most of the time?) it involves incompatible
changes.
I have code from last summer that do not work
anymore.
Moreover the freeze period is to short for us to react
and test our plugin.
Fast!
Too fast?
4th february 2011 Loïc Fejoz 18/19
19. Conclusion
● Interesting platform
● Lots of plugins
● Models need more semantic checking
● To few documentation
● Not stable enough
● NIH syndrom (between EMF and core)
4th february 2011 Loïc Fejoz 19/19