The "UML&FM’2009" workshop was followed by 30 people, during the whole day of december the 8th, from 09:00 to 17:30.
It was composed of four sessions: SESSION 1: Generic aspects , SESSION 2: Integration , SESSION 3: Executable Platforms, SESSION 4: Real-time, embedded and complex systems and fifteen presentations.
Among these sessions we have selected in each the most popular with some promising questions.
- SESSION 1: In ""Dealing With Variability Within a Family Of Domain Specific Languages: Comparative Analysis Of Various Techniques" , Christian Percebois (from IRIT, France) was asked the following question: Dealing with variability entails different formalisms in order to integrate specific semantics. How to adapt your approach actually only based on algebraic specifications in order to be able to integrate such constraints? Christian Percebois answered that since about ten years now, a whole formal framework exists making it possible to deal with the heterogeneity of specification formalisms. This last was defined within the framework of the institutions by Goguen and Burstall and consists in extending a traditional construction in the category theory and to flat a set of logical formalisms in a more total way. If Christian Percebois’team would like to integrate formal specifications that use various formalisms, we would have to extend our framework to the use of institutions. Christian Percebois’team has not done this yet, but we intend to look at this issue in the future.
- SESSION 2: In "A First Attempt to Combine SysML Requirements Diagrams and B", Régine Laleau (from Université Paris 12, France), answered to a question from Renato Silva: What do you consider the B formal method and not Event-B ? The author answer was that the main reason is that the structuration mechanisms in B are better adapted to your project than those of Event-B. Renato Silva replied that in his PhD, he has developed new ones that can fit you. The question was very relevant and Régine Laleau’s team plan to study the Renato’s proposition in her project.
- SESSION 3: In "Formal Executable Semantics for Conformance in the MDE Framework", Vlad Rusu (from INRIA, France) answered to the question "why use Maude" (and not Prolog, for instance) for the purpose of the work he presented (for checking model-to-metamodel conformance). Vlad Rusu believes this kind of question is always challenging because one always has his/her preference and background in terms of methods/tools, and we are all inclined to use (and like... ) what we know, for the obvious reason. Yet, this cannot constitute a reasonable scientific answer...He thinks he managed to give a (hopefully) more convincing answer along the lines of "in Maude there is the notion of theory interpretation, which adequately captures the intuitive idea that models are interpretations of meta-models". Implicitly, that the MDE definitions are easily captured in Maude, without need to too much "twisting" them to enter the framework.
- SESSION 4: In "UML Modeling and Formal Verification of Secure Group Communication Protocols", Pierre de Saqui-Sannes (from ISAE, France) was asked how large where the group of Humans managed by the model you formally verified? Did you quickly face the state explosion problem? The author’s answer was that the SAFECAST system manages groups of Human who communicate using PMR radios. A message sent by a group member is broadasted and received by all other members at the same time. Formal verification has therefore been achieved using small groups of Human. Managing large group of Human deserves investigation in new techniques. They are currently working on joint use of real-time UML and network calculus.
- During the presentation "Lightweight Analysis of Access Control Models with Description Logic" by Christiano Braga (from Niterói, Brazil) , there was an iteresting comment by Dorel Lucanu suggesting that the paper below could provide good insights on how a non-monotonic logic could be used in connection with the approach described in the paper that Christiano Braga co-authored and presented at the UML&FM’09 workshop. Christiano Braga’s team have not yet studied the approach in the suggested paper however they believe that a open world assumption (and therefore the use of a monotonic logic) is important to their approach. The paper that Dorel suggested is entitled "Can OWL and logic programming live together happily ever after?" (2006) by Boris Motik, Ian Horrocks, Riccardo Rosati and Ulrike Sattler. Dorel Lucanu also added that the following paper of Boris Motik and Riccardo Rosati. "A faithful integration of description logics with logic programming" In \em IJCAI-07, pages 477—482, 2007, is also strong related to that topic. Dorel Lucanu rephrased a comment he made in Rio during a short talk with Christiano. In his opinion, Open World Assumption (OWA) on DL is miss-understood in the sense that it lets to much freedom to define models.
It does not make sense to consider a model whose the carrier set consists of number in order to give semantics to a food ontology. It is more appropriate to consider only "extended Herbrand models", which roughly speaking are Herbrand models extended with a countable set of constants. This idea is also used in the two papers he mentioned. From theoretical point of view, this is not a restriction (see, e.g., Theorem 5.9.4 in Melvin Fitting, First-order logic and automated theorem proving, Springer, 1996, 2nd edition). This approach is very convenient when they want to combine DL with a non-monotonic logic, let denote it by NML, since the semantics of the specifications in NML is usually given in terms of Herbrand models. For instance, you may consider specifications (O, P) combining an ontology in DL with a specification P in NML. Then a (O,P)-model M is just an O-model M_O "enriched" according to the semantics of P. If you can express M_O as a NML-formula \phi, then M is in fact a (P \cup \phi)-model and a tool for NML can be used for reasoning about the combined specifications.