Introduction to special issue: papers from UML&FM'2011

test case generation (symbolic execution of the mo-del), concretization (generation of executable test scripts from abstract test cases) and analysis (assignation of the test verdict). This process is automated by a toolchain based on Topcased modeler, Smartesting test generator and Clemessy TestInView. In UML / SysML semantic tunings, Ileana Ober, Iulian Ober, Iulia Dragomir and El Arbi Aboussoror describe how applying their framework on large industrial models revealed the fact that some features of the UML/SysML semantics which lead to bottlenecks in verification are not actually necessary in the models that they have considered, thus leaving place for optimisations. Their paper discusses the gap existing between the choices made in the general UML/SysML semantic framework and the actual needs of the users. They illustrate it based on the semantics of ports, for which they give a simplified version of the semantics. In Formal verification of components assembly based on SysML and interface automata, Samir Chouali and Ahmed Hammad propose an approach which combines component SysML models and interface automata in order to assemble components and to verify formally their interoperability. They specify component-based system architecture with component SysML Block definition diagrams, and the composition links between components with Internal Block Diagrams. Components protocols are specified with sequence diagrams, they are necessary to exploit interface automata formalism. Interface automata is a common Input Output (I/O) automata-based formalism intended to specify the signature and the protocol level of component interfaces. 3 Session 3: Z, B and OCL In Test Data Generation for Web Application using a UML Class Diagram with OCL Constraints, Shoichiro Fujiwara, Kazuki Munakata, Tadahiro Uehara, Yoshiharu Maeda and Asako Katayama present their current work toward efficient and effective verification ofweb applications. Their approach begins with formally representing specifications in a basic design phase. This paper argues that application behaviors in the basic design can be expressed by states of screen and database around events like screen transitions. They use a UML class diagram with OCL to describe the application behaviors and data constraints. In Coupling-based UML Transformations of Formal Z Specifications, Andreas Bollin demonstrates by the example of formal Z, that the utilization of measures can play an important role during forward as well as reverse engineering activities. It suggests tomakeuse of coupling-basedmeasures and shows how to overcome parts of existing impediments. The basic idea is to optimize the values of coupling for all related operations.With that two issues are addressed: firstly, the mapping of operations to classes and methods is based on reproducible measures that are intuitively comprehensible. Secondly, due to maximizing the values for coupling between methods within a class, a possible deferred implementation also very likely has comparable properties. InA Proposal for Extending UML-B to Support a Conceptual Model, Thiago C. De Sousa, Colin F. Snook and Paulo SergioMuniz Silva present a proposal for extending UML-B to support a conceptual model in order to provide an easier starting point for the actual development process. More precisely, they propose two diagrams to facilitate the passing from requirements to the initial formal model: a first one to represent system behavior based onUML2 InteractionOverview Diagram (IOD) and a second one for system structure based on Boundary–Control–Entity Stereotyped Class Diagram (BCE). They show how to translate the former into an Event-B specification and explain how to link the latter to the original UML-B using a simple ATM example as case study. In Combining UML and B for the Formal Specification of an Access Control Filter, Jeremy Milhau, Akram Idani, Regine Laleau, Mohamed Amine Labiadh, Yves Ledru and Marc Frappier present a methodology to specify access control policies starting by a set of graphical diagrams: UML for the functional model, SecureUML for static access control and ASTD for dynamic access control. These diagrams are translated into a set of B machines. Finally, the authors present the formal specification of an access control filter that coordinates the different kinds of access control rules and the specification of functional operations. 4 Session 4: UML2 State Machines In Institutionalising UML 2.0 State Machines, Daniel Calegari and Nora Szasz define an institution for UML 2.0 State Machines. The building blocks of their institution are based on a previous semantics dealingwith processing simple input events within a transition step. They also extend these semantic definitions for handling sequences of events, and then for considering runs through the state machine. 5 Overview of a new action language standard In Alf formal, Isabelle Perseil describes the state-of-the-art of the new action language for Foundational UML, with its advantages and drawbacks. The author concludes by stating that it is very important to use a languagewhich allows a good integration with formal methods; therefore, the Alf language should be extended for the need of critical systems design. Acknowledgments Theorganizerswould like to thankMikeHinchey, Emil Vassev and David Sinclair for their support and their advices for the successful organization of this workshop.